Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-26 11:17 2c698bd1

View on Github →

docs(set_theory/zfc): add module docstring and missing def docstrings (#8744)

Estimated changes

Modified src/set_theory/zfc.lean

modified def Class.fval

modified def Class.iota

modified theorem Class.iota_val

modified def Class.to_Set

modified theorem Set.Union_lem

modified theorem Set.choice_mem_aux

modified theorem Set.eq_empty

modified theorem Set.ext

modified theorem Set.ext_iff

modified theorem Set.induction_on

modified theorem Set.mem_empty

modified theorem Set.mem_image

modified theorem Set.mem_prod

modified def Set.prod

modified def arity

modified def pSet.embed

added theorem pSet.equiv.rfl

modified theorem pSet.equiv_iff_mem

modified theorem pSet.mem.congr_left

modified theorem pSet.mem.congr_right

modified theorem pSet.mem.ext

modified theorem pSet.mem_Union

modified theorem pSet.mem_empty

modified theorem pSet.mem_image

modified def pSet.omega

modified def pSet.resp