subset_range_iff_exists_image_eq — Mathlib

English

For any f: α → β and s ⊆ β, s ⊆ range f iff ∃ t, f''t = s.

Русский

Для любой функции f и подмножества s ⊆ β следует, что s ⊆ range f тогда и только тогда, когда ∃ t, f''t = s.

LaTeX

$$$ s \\subseteq \\mathrm{range}(f) \\iff \\exists t, \\mathrm{image}(f)(t) = s. $$$

Lean4

theorem subset_range_iff_exists_image_eq {f : α → β} {s : Set β} : s ⊆ range f ↔ ∃ t, f '' t = s :=
  ⟨fun h => ⟨_, image_preimage_eq_iff.2 h⟩, fun ⟨_, ht⟩ => ht ▸ image_subset_range _ _⟩

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