Theorems · Theorem · logic and foundations
FirstOrder.Language.Formula.realize_relabel_sumInr
∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {n : ℕ} (φ : L.Formula (Fin n)) {v : Empty → M}
{x : Fin n → M}, (FirstOrder.Language.BoundedFormula.relabel Sum.inr φ).Realize v x ↔ φ.Realize x- Defined in
- Mathlib.ModelTheory.Semantics
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 55 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- FirstOrder.Languagestatement and proof · cited by 1,084
- FirstOrder.Language.Structurestatement and proof · cited by 775
- FirstOrder.Language.BoundedFormula.Realizestatement and proof · cited by 104
- FirstOrder.Language.Formulastatement and proof · cited by 93
- FirstOrder.Language.Formula.Realizestatement and proof · cited by 81
- FirstOrder.Language.BoundedFormula.relabelstatement · cited by 17
- FirstOrder.Language.BoundedFormula.realize_relabelproof · cited by 3
Cited by1
Results whose statement or proof uses this declaration.
- FirstOrder.Language.Embedding.isElementary_of_existsproof · cited by 1