Commit 2023-10-26 10:03 d03396c1

View on Github →

feat: Lattice closedness (#7548) Define when a set in a lattice is closed under lattice operations.

Estimated changes

Modified Mathlib/Order/Closure.lean

added theorem ClosureOperator.closed_ofPred

added theorem ClosureOperator.mem_closed_ofPred

added def ClosureOperator.ofPred

added theorem ClosureOperator.ofPred_spec

Modified Mathlib/Order/SupClosed.lean

added theorem InfClosed.image

added theorem InfClosed.preimage

added theorem InfClosed.prod

added theorem IsSublattice.image

added theorem IsSublattice.inter

added theorem IsSublattice.preimage

added theorem IsSublattice.prod

added structure IsSublattice

added theorem IsSublattice_range

added theorem Set.Finite.latticeClosure

added theorem SupClosed.image

added theorem SupClosed.preimage

added theorem SupClosed.prod

added theorem finsetInf'_mem_infClosure

added theorem finsetSup'_mem_supClosure

added theorem infClosed_pi

modified theorem infClosed_preimage_ofDual

modified theorem infClosed_preimage_toDual

added theorem infClosed_range

added theorem infClosure_closed

added theorem infClosure_min

added theorem infClosure_supClosure

added theorem inf_mem_infClosure

added theorem isSublattice_empty

added theorem isSublattice_iInter

added theorem isSublattice_latticeClosure

added theorem isSublattice_pi

added theorem isSublattice_preimage_ofDual

added theorem isSublattice_preimage_toDual

added theorem isSublattice_sInter

added theorem isSublattice_singleton

added theorem isSublattice_univ

added def latticeClosure

added theorem latticeClosure_closed

added theorem latticeClosure_empty

added theorem latticeClosure_eq_self

added theorem latticeClosure_idem

added theorem latticeClosure_min

added theorem latticeClosure_mono

added theorem latticeClosure_singleton

added theorem latticeClosure_univ

added theorem subset_latticeClosure

added theorem supClosed_pi

modified theorem supClosed_preimage_ofDual

modified theorem supClosed_preimage_toDual

added theorem supClosed_range

added theorem supClosure_closed

added theorem supClosure_infClosure

added theorem supClosure_min

added theorem sup_mem_supClosure