Commit 2024-04-04 00:36 89a00da8

View on Github →

Feat: Add some operations and lemmas on closure operators/order homs (#10348) This adds conjugation of order homomorphisms & closure operators by order isos, as well as two new extensionality lemmas for closure operators, a proof that the inf of a closed family is closed, and that the closure of an element is the GLB of all closed elements larger than it. There is also includes some minor refactoring, moving Set.image_sSup from Mathlib/Order/Hom/CompleteLattice to Mathlib/Data/Set/Lattice and adding some common lemmas for EquivLike-things to OrderIso.

Estimated changes

Modified Mathlib/Data/Set/Lattice.lean

added theorem Set.image_sUnion

Modified Mathlib/Order/Closure.lean

added theorem ClosureOperator.closure_isGLB

added def ClosureOperator.conjBy

added theorem ClosureOperator.conjBy_refl

added theorem ClosureOperator.conjBy_trans

modified theorem ClosureOperator.ext

added theorem ClosureOperator.ext_isClosed

added theorem ClosureOperator.sInf_isClosed

added def OrderIso.equivClosureOperator

Modified Mathlib/Order/Hom/Basic.lean

added def OrderIso.arrowCongr

added def OrderIso.conj

added theorem OrderIso.self_trans_symm

added theorem OrderIso.symm_trans_self

Modified Mathlib/Order/Hom/CompleteLattice.lean

modified theorem Set.image_sSup

Modified Mathlib/Order/RelIso/Basic.lean

added theorem RelIso.self_trans_symm

added theorem RelIso.symm_trans_self