Theorems · Theorem · logic and foundations
FirstOrder.Language.Substructure.realize_formula_top
∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u_3} {φ : L.Formula α} {v : α → ↥⊤},
φ.Realize v ↔ φ.Realize (Subtype.val ∘ v)- Defined in
- Mathlib.ModelTheory.Substructures
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 25 from the axioms · uses propext, Quot.sound
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.
- Top.topstatement and proof · cited by 9,680
- FirstOrder.Languagestatement and proof · cited by 1,084
- FirstOrder.Language.Structurestatement and proof · cited by 775
- FirstOrder.Language.Substructurestatement · cited by 242
- FirstOrder.Language.Formulastatement and proof · cited by 93
- FirstOrder.Language.Formula.Realizestatement and proof · cited by 81
- FirstOrder.Language.Substructure.topEquivproof · cited by 4
- FirstOrder.Language.StrongHomClass.realize_formulaproof · cited by 2
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.