cg_iff_structure_cg — Mathlib

English

For a language L and substructure S of M, CG in S coincides with CG in the induced structure on S; i.e., S.CG ↔ Structure.CG L S.

Русский

Для языка L и подструктуры S множества S.CG совпадает с CG относительно индуцированной структуры; т. е. S.CG ↔ Structure.CG L S.

LaTeX

$$$$ S.CG \iff Structure.CG\ L\ S. $$$$

Lean4

theorem cg_iff_structure_cg (S : L.Substructure M) : S.CG ↔ Structure.CG L S :=
  by
  rw [Structure.cg_def]
  refine ⟨fun h => CG.of_map_embedding S.subtype ?_, fun h => ?_⟩
  · rw [← Hom.range_eq_map, range_subtype]
    exact h
  · have h := h.map S.subtype.toHom
    rw [← Hom.range_eq_map, range_subtype] at h
    exact h

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