fg_iff — Mathlib

English

Equivalences exist between FG and CG under language-equivalences; FG is preserved by equivalences.

Русский

Существуют эквивалентности между FG и CG под эквивалентностями языка; FG сохраняется при эквивалентностях.

LaTeX

$$$$ (f : L\\text{-equiv } M N) \\Rightarrow (FG\\;L\\;M \\Leftrightarrow FG\\;L\\;N). $$$$

Lean4

theorem fg_iff {N : Type*} [L.Structure N] (f : M ≃[L] N) : Structure.FG L M ↔ Structure.FG L N :=
  ⟨fun h => h.map_of_surjective f.toHom f.toEquiv.surjective, fun h =>
    h.map_of_surjective f.symm.toHom f.toEquiv.symm.surjective⟩

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