sUnion_mono_subsets — Mathlib

English

If t ⊆ f t for all t, then ⋃S ⊆ ⋃(f''S).

Русский

Если для всех t выполняется t ⊆ f(t), то ⋃S ⊆ ⋃(f''S).

LaTeX

$$$ (\forall t : Set α, t \subseteq f t) \Rightarrow \bigcup S \subseteq \bigcup (f '' S) $$$

Lean4

/-- `sUnion` is monotone under taking a subset of each set. -/
theorem sUnion_mono_subsets {s : Set (Set α)} {f : Set α → Set α} (hf : ∀ t : Set α, t ⊆ f t) : ⋃₀ s ⊆ ⋃₀ (f '' s) :=
  fun _ ⟨t, htx, hxt⟩ ↦ ⟨f t, mem_image_of_mem f htx, hf t hxt⟩

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