map_generate_le_generate_preimage_preimage

English

Let U be a collection of β-subsets and f: β → α. Then map f of generate U is less than or equal to generate of the preimage family: map f (generate U) ≤ generate ((f ⁻¹' ·) ⁻¹' U).

Русский

Пусть U—периодический набор подмножеств β, и f: β → α. Тогда map f от generate U меньше или равно generate ((f⁻¹'·)⁻¹' U).

LaTeX

$$$ \operatorname{map} f (\operatorname{generate} U) \le \operatorname{generate} \bigl(((f^{-1} \cdot)^{-1}) U\bigr) $$$

Lean4

theorem map_generate_le_generate_preimage_preimage (U : Set (Set β)) (f : β → α) :
    map f (generate U) ≤ generate ((f ⁻¹' ·) ⁻¹' U) :=
  by
  rw [le_generate_iff]
  exact fun u hu ↦ mem_generate_of_mem hu

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