sUnion_mono_supsets — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- `sUnion` is monotone under taking a superset of each set. -/
theorem sUnion_mono_supsets {s : Set (Set α)} {f : Set α → Set α} (hf : ∀ t : Set α, f t ⊆ t) : ⋃₀ (f '' s) ⊆ ⋃₀ s :=
  -- If t ∈ f '' s is arbitrary; t = f u for some u : Set α.
   fun _ ⟨_, ⟨u, hus, hut⟩, hxt⟩ ↦ ⟨u, hus, (hut ▸ hf u) hxt⟩

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