range_eq_empty_of_isEmpty — Mathlib

English

If α is empty, then for any simple function f : α → β, f.range = ∅.

Русский

Если α пуст, то для любой простой функции f : α → β область значений пустого множества: f.range = ∅.

LaTeX

$$$\\text{IsEmpty }\\alpha \\Rightarrow f.\\mathrm{range} = \\emptyset.$$$

Lean4

@[simp]
theorem range_eq_empty_of_isEmpty {β} [hα : IsEmpty α] (f : α →ₛ β) : f.range = ∅ :=
  by
  rw [← Finset.not_nonempty_iff_eq_empty]
  by_contra h
  obtain ⟨y, hy_mem⟩ := h
  rw [SimpleFunc.mem_range, Set.mem_range] at hy_mem
  obtain ⟨x, hxy⟩ := hy_mem
  rw [isEmpty_iff] at hα
  exact hα x

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