cg_iff — Mathlib

English

Equivalences preserve CG between L-structures M and N.

Русский

Эквивалентности сохраняют cg между L-структурами M и N.

LaTeX

$$$$ \\text{If } f: M \\simeq_L N, \\; CG_L M \\iff CG_L N. $$$$

Lean4

theorem cg_iff {N : Type*} [L.Structure N] (f : M ≃[L] N) : Structure.CG L M ↔ Structure.CG 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⟩

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