dom_fg_iff_cod_fg — Mathlib

English

For a partial equivalence f, dom and cod FG properties are equivalent: f.dom.FG ↔ f.cod.FG.

Русский

Для частичной эквивалентности f свойства FG области определения и кодомы эквивалентны: f.dom.FG ↔ f.cod.FG.

LaTeX

$$$\forall f : M \equiv_p^L N,\; f.\mathrm{dom}.FG \;\iff\; f.\mathrm{cod}.FG.$$$

Lean4

theorem dom_fg_iff_cod_fg {N : Type*} [L.Structure N] (f : M ≃ₚ[L] N) : f.dom.FG ↔ f.cod.FG := by
  rw [Substructure.fg_iff_structure_fg, f.toEquiv.fg_iff, Substructure.fg_iff_structure_fg]

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