Commit 2023-05-01 08:43 7b35d8f0

View on Github →

feat: port ZFC set intersection (#3345) Also fixes some erroneous theorem names from the port. set_theory.zfc.basic@98bbc3526516bca903bff09ea10c4206bf079e6b..f0b3759a8ef0bd8239ecdaa5e1089add5feebe1a Mathlib 3: https://github.com/leanprover-community/mathlib/pull/18232

Estimated changes

added theorem Class.coe_interₛ
added def Class.interₛ
added theorem Class.interₛ_apply
added theorem Class.interₛ_empty
added theorem Class.mem_interₛ
added theorem Class.toSet_of_ZFSet
deleted theorem Class.toSet_of_setCat
modified theorem Class.unionₛ_empty
added theorem ZFSet.interₛ_empty
added theorem ZFSet.mem_interₛ
added theorem ZFSet.toSet_interₛ
added theorem ZFSet.toSet_unionₛ
deleted theorem ZFSet.to_set_unionₛ
modified theorem ZFSet.unionₛ_empty