image_eq_range — Mathlib

English

Let f: α → β and s ⊆ α. Then f '' s equals the range of the restricted function x ↦ f x on s.

Русский

Пусть f: α → β и s ⊆ α. Тогда f '' s равно диапазону функции x ↦ f x на s.

LaTeX

$$$$ f''s = \\operatorname{range}(\\lambda x : s, f\\, x) $$$$

Lean4

theorem image_eq_range (f : α → β) (s : Set α) : f '' s = range fun x : s => f x :=
  by
  ext
  constructor
  · rintro ⟨x, h1, h2⟩
    exact ⟨⟨x, h1⟩, h2⟩
  · rintro ⟨⟨x, h1⟩, h2⟩
    exact ⟨x, h1, h2⟩

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