subset_image_union — Mathlib

English

The image of the union s ∪ f^{-1}(t) is contained in the union f(s) ∪ t: f''(s ∪ f^{-1}(t)) ⊆ f'' s ∪ t.

Русский

Образ объединения s ∪ f^{-1}(t) содержится в объединении f(s) ∪ t: f''(s ∪ f^{-1}(t)) ⊆ f'' s ∪ t.

LaTeX

$$$f''(s \\cup f^{-1}(t)) \\subseteq f'' s \\cup t$$$

Lean4

theorem subset_image_union (f : α → β) (s : Set α) (t : Set β) : f '' (s ∪ f ⁻¹' t) ⊆ f '' s ∪ t :=
  image_subset_iff.2 (union_preimage_subset _ _ _)

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