search

metamath / set.mm

Metamath source file for logic and set theory
Creative Commons Zero v1.0 Universal
238 stars 87 forks source link

wl-df3maxtru1 #4059

Closed wlammen closed 3 weeks ago

wlammen commented 3 weeks ago
  1. Point out in comments different interpretations of n-mintru-m.
  2. add wl-df3maxtru1 as a theorem addressing 'mutual exclusivity' in propositional expressions