is_equiv_invariant — Mathlib

English

If there is an L-equivalence between M and N, then the ages of M and N are equal.

Русский

Если между M и N существует эквивалентность по языку L, тогда возраста M и N равны.

LaTeX

$$$\text{age}_L(M) = \text{age}_L(N)$ whenever $M \cong_L N$.$$

Lean4

theorem is_equiv_invariant (N P : Bundled.{w} L.Structure) (h : Nonempty (N ≃[L] P)) : N ∈ L.age M ↔ P ∈ L.age M :=
  and_congr h.some.fg_iff
    ⟨Nonempty.map fun x => Embedding.comp x h.some.symm.toEmbedding,
      Nonempty.map fun x => Embedding.comp x h.some.toEmbedding⟩

Похожие утверждения