Theorems · Theorem · logic and foundations
FirstOrder.Language.structure_simpleGraphOfStructure
∀ {V : Type u} [S : FirstOrder.Language.graph.Structure V] [inst : V ⊨ FirstOrder.Language.Theory.simpleGraph],
(FirstOrder.Language.simpleGraphOfStructure V).structure = S- Defined in
- Mathlib.ModelTheory.Graph
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 41 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Matrix.vecEmptyproof · cited by 832
- FirstOrder.Language.Structurestatement and proof · cited by 775
- Matrix.cons_val_fin_oneproof · cited by 225
- FirstOrder.Language.Functionsproof · cited by 153
- FirstOrder.Language.Relationsproof · cited by 147
- FirstOrder.Language.Structure.RelMapproof · cited by 68
- FirstOrder.Language.Theory.Modelstatement and proof · cited by 67
- isEmptyElimproof · cited by 59
- iff_eq_eqproof · cited by 13
- FirstOrder.Language.Theory.simpleGraphstatement and proof · cited by 4
- FirstOrder.Language.graphstatement and proof · cited by 4
- FirstOrder.Language.simpleGraphOfStructurestatement · cited by 3
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.