preimage_const_of_mem — Mathlib

English

For a fixed b in β and any set s, the preimage of s under the constant function mapping every input to b is universal provided b ∈ s.

Русский

Для фиксированного b ∈ β и любого множества s обратное образ константной функции, посылающей каждый аргумент в b, равняется вселенной при условии b ∈ s.

LaTeX

$$$\{x : \alpha \mid (\text{const } b)(x) \in s\} = \mathrm{univ}$ when $b \in s$.$$

Lean4

@[simp]
theorem preimage_const_of_mem {b : β} {s : Set β} (h : b ∈ s) : (fun _ : α => b) ⁻¹' s = univ :=
  eq_univ_of_forall fun _ => h

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