generate_image_preimage_le_comap — Mathlib

English

Let U be a family of β-subsets and f: β → α. Then generate ((f ⁻¹' ·) '' U) ≤ comap f (generate U).

Русский

Пусть U—семейство подмножеств β и f: β → α. Тогда generate ((f⁻¹'·)'' U) ≤ comap f (generate U).

LaTeX

$$$ \operatorname{generate}(((f^{-1} \cdot)'' U)) \le \operatorname{comap} f (\operatorname{generate} U) $$$

Lean4

theorem generate_image_preimage_le_comap (U : Set (Set α)) (f : β → α) :
    generate ((f ⁻¹' ·) '' U) ≤ comap f (generate U) :=
  by
  rw [← map_le_iff_le_comap, le_generate_iff]
  exact fun u hu ↦ mem_generate_of_mem ⟨u, hu, rfl⟩

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