map — Mathlib

English

Under a mild assumption on the language, a substructure is CG if and only if it is countable.

Русский

При некоторых предпосылках относительно языка подструктура CG тогда и только тогда, когда она счётна.

LaTeX

$$$\text{cg}_\text{countable} \ :\ s.CG \iff \text{Countable}(s)$$$

Lean4

theorem map {N : Type*} [L.Structure N] (f : M →[L] N) {s : L.Substructure M} (hs : s.CG) : (s.map f).CG :=
  let ⟨t, ht⟩ := cg_def.1 hs
  cg_def.2 ⟨f '' t, ht.1.image _, by rw [closure_image, ht.2]⟩

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