Theorems · Theorem · logic and foundations

FirstOrder.Language.Substructure.closure_eq_of_le

∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {S : L.Substructure M} {s : Set M},
  s ⊆ ↑S →
    S ≤ (FirstOrder.Language.Substructure.closure L).toFun s → (FirstOrder.Language.Substructure.closure L).toFun s = S

Defined in: Mathlib.ModelTheory.Substructures
Cited by: 5 results in Mathlib
Foundations: Depth 69 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: FirstOrder.Language.Structure

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites8

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
SetLike.coestatement and proof · cited by 8,199
FirstOrder.Languagestatement and proof · cited by 1,084
FirstOrder.Language.Structurestatement and proof · cited by 775
FirstOrder.Language.Substructurestatement and proof · cited by 242
LowerAdjoint.toFunstatement and proof · cited by 105
FirstOrder.Language.Substructure.closurestatement and proof · cited by 70
LowerAdjoint.eq_of_leproof · cited by 2

Cited by5

Results whose statement or proof uses this declaration.

FirstOrder.Language.Substructure.map_closureproof · cited by 4
FirstOrder.Language.Substructure.coe_closure_eq_range_term_realizeproof · cited by 3
FirstOrder.Language.Substructure.mem_closed_iffproof · cited by 1
FirstOrder.Language.Substructure.cg_iff_empty_or_exists_nat_generating_familyproof · cited by 0
FirstOrder.Language.Substructure.closure_withConstants_eqproof · cited by 0