Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-01-25 06:17
9d2da635
View on Github →
feat(Order/Nucleus): Nucleus (
#19440
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/Order/Nucleus.lean
added
theorem
Nucleus.bot_apply
added
theorem
Nucleus.coe_bot
added
theorem
Nucleus.coe_le_coe
added
theorem
Nucleus.coe_lt_coe
added
theorem
Nucleus.coe_toInfHom
added
theorem
Nucleus.coe_top
added
theorem
Nucleus.ext
added
theorem
Nucleus.idempotent
added
theorem
Nucleus.le_apply
added
theorem
Nucleus.map_inf
added
def
Nucleus.toClosureOperator
added
theorem
Nucleus.toFun_eq_coe
added
theorem
Nucleus.top_apply
added
structure
Nucleus