Theorems · Theorem · logic and foundations

FirstOrder.Language.Hereditary.is_equiv_invariant_of_fg

∀ {L : FirstOrder.Language} {K : Set (CategoryTheory.Bundled L.Structure)},
  FirstOrder.Language.Hereditary K →
    (∀ M ∈ K, FirstOrder.Language.Structure.FG L ↑M) →
      ∀ (M N : CategoryTheory.Bundled L.Structure), Nonempty (L.Equiv ↑M ↑N) → (M ∈ K ↔ N ∈ K)

Defined in: Mathlib.ModelTheory.Fraisse
Cited by: 2 results in Mathlib
Foundations: Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites11

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
FirstOrder.Languagestatement and proof · cited by 1,084
FirstOrder.Language.Structurestatement and proof · cited by 775
CategoryTheory.Bundled.αstatement and proof · cited by 736
Nonempty.someproof · cited by 340
FirstOrder.Language.Equivstatement and proof · cited by 83
CategoryTheory.Bundledstatement and proof · cited by 42
FirstOrder.Language.Equiv.symmproof · cited by 32
FirstOrder.Language.Structure.FGstatement and proof · cited by 27
FirstOrder.Language.Hereditarystatement and proof · cited by 5
FirstOrder.Language.Structure.FG.mem_age_of_equivproof · cited by 1

Cited by2

Results whose statement or proof uses this declaration.

FirstOrder.Language.exists_cg_is_age_ofproof · cited by 1
FirstOrder.Language.IsFraisse.is_equiv_invariantproof · cited by 0