Mathlib Map

Theorems · Theorem · order theory

IsSublattice.supClosed

∀ {α : Type u_3} [inst : Lattice α] {s : Set α}, IsSublattice s → SupClosed s
Defined in
Mathlib.Order.SupClosed
Cited by
15 results in Mathlib
Foundations
Depth 5 from the axioms · uses no axioms
Assumes
Lattice
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

four_functions_theorem · cited by 3four_functions_theoremsupClosure_infClosure · cited by 2supClosure_infClosurelatticeClosure_sup_inf_induction · cited by 1latticeClosure_sup_inf_in…isSublattice_preimage_ofDual · cited by 1isSublattice_preimage_ofD…isSublattice_preimage_toDual · cited by 1isSublattice_preimage_toD…isSublattice_sInter · cited by 1isSublattice_sInterimage_latticeClosure · cited by 1image_latticeClosureBooleanSubalgebra.mem_closure_iff_sup_sdiff · cited by 1BooleanSubalgebra.mem_clo…IsSublattice.image · cited by 0IsSublattice.imageIsSublattice.inter · cited by 0IsSublattice.interIsSublattice.preimage · cited by 0IsSublattice.preimageIsSublattice.prod · cited by 0IsSublattice.prodinfClosure_supClosure · cited by 0infClosure_supClosureisSublattice_iInter · cited by 0isSublattice_iInterisSublattice_pi · cited by 0isSublattice_piSet · cited by 53352SetLattice · cited by 916LatticeSupClosed · cited by 57SupClosedIsSublattice · cited by 28IsSublatticeIsSublattice.supClosedCITED BYCITES

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Setstatement and proof · cited by 53,352
  • Latticestatement and proof · cited by 916
  • SupClosedstatement · cited by 57
  • IsSublatticestatement and proof · cited by 28

Cited by16

Results whose statement or proof uses this declaration.