comap — Mathlib

English

If β is countably generated and f: α → β, then the comap of m along f is countably generated.

Русский

Если β счетно порождается и есть отображение f: α → β, то comap f m счетно порождается.

LaTeX

$$$ \text{comap} : \text{CountablyGenerated } α \to \text{CountablyGenerated } α $$$

Lean4

theorem comap [m : MeasurableSpace β] [h : CountablyGenerated β] (f : α → β) : @CountablyGenerated α (.comap f m) :=
  by
  rcases h with ⟨⟨b, hbc, rfl⟩⟩
  rw [comap_generateFrom]
  letI := generateFrom (preimage f '' b)
  exact ⟨_, hbc.image _, rfl⟩

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