Mathlib v3 is deprecated. Go to Mathlib v4

Theorem Class.ext_iff

Modification history

2023-03-28 07:28

src/set_theory/zfc/basic.lean

feat(set_theory/zfc/basic): simpler/more general `Class.ext` (#18306) …

Modified Class.ext_iff View on Github →

2023-01-25 14:10

src/set_theory/zfc/basic.lean

feat(set_theory/zfc/basic): more basic simp/ext lemmas (#18233) …

Added Class.ext_iff View on Github →