Theorems · Theorem · logic and foundations

FirstOrder.Language.Substructure.comap_inf_map_of_injective

∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N] {f : L.Hom M N},
  Function.Injective ⇑f →
    ∀ (S T : L.Substructure M),
      FirstOrder.Language.Substructure.comap f
          (FirstOrder.Language.Substructure.map f S ⊓ FirstOrder.Language.Substructure.map f T) =
        S ⊓ T

Defined in

Mathlib.ModelTheory.Substructures

Cited by

0 results in Mathlib

Foundations

Depth 67 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FirstOrder.Language.StructureFirstOrder.Language.Structure