range_eq_singleton_iff — Mathlib

English

If Nonempty ι, then range f = { y } iff ∀ x, f x = y.

Русский

Если ι непуст, то range f равно одному элементу {y} тогда и только тогда, когда для всех x выполняется f(x) = y.

LaTeX

$$$ \\operatorname{range} f = \\{ y \\} \\;\\iff\\; \\forall x:\\, ι,\\ f(x) = y$$$

Lean4

@[simp]
theorem range_eq_singleton_iff [Nonempty ι] {y} : Set.range f = { y } ↔ ∀ (x : ι), f x = y :=
  by
  simp_rw [Set.ext_iff, Set.mem_range, Set.mem_singleton_iff]
  exact ⟨fun h _ => by simp_rw [← h, exists_apply_eq_apply], fun h _ => by simp_rw [h, exists_const, eq_comm]⟩

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