preimage_const — Mathlib

English

Let f: α → β be the constant function f(x) = b. Then (f)^{-1}(s) equals univ if b ∈ s, and equals ∅ if b ∉ s.

Русский

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

LaTeX

$$$ (\\{ x \\in \\alpha \\mid b \\in s \\}) = \\begin{cases} \\alpha, & b \\in s \\\\ \\emptyset, & b \\notin s \\end{cases}. $$$

Lean4

theorem preimage_const (b : β) (s : Set β) [Decidable (b ∈ s)] : (fun _ : α => b) ⁻¹' s = if b ∈ s then univ else ∅ :=
  by grind

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