preimage_const_of_notMem — Mathlib

English

Let f: α → β be the constant function f(x) = b. If b ∉ s, then f^{-1}(s) = ∅.

Русский

Пусть f: α → β является константной функцией f(x) = b. Если b ∉ s, то f^{-1}(s) = ∅.

LaTeX

$$$ b \\notin s \\Rightarrow \\{ x \\in \\alpha \\mid b \\in s \\} = \\emptyset.$$$

Lean4

@[simp]
theorem preimage_const_of_notMem {b : β} {s : Set β} (h : b ∉ s) : (fun _ : α => b) ⁻¹' s = ∅ :=
  eq_empty_of_subset_empty fun _ hx => h hx

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