Commit 2023-04-01 16:28 93bf16ce

View on Github →

chore: Miscellaneous lemmas (#3213) Match https://github.com/leanprover-community/mathlib/pull/18677

Estimated changes

added theorem Function.support_one
added theorem Int.cast_eq_one
added theorem Int.cast_ne_one
added theorem Set.inter_setOf_eq_sep
added theorem Set.setOf_inter_eq_sep
added theorem Function.onFun_apply
added theorem WithBot.infₛ_eq
added theorem WithBot.supₛ_eq
added theorem WithTop.infₛ_eq
added theorem WithTop.supₛ_eq