preimage_one — Mathlib

English

Let s ⊆ β and consider the constant map 1: α → β. Then the preimage 1^{-1}(s) equals s contains 1 or not; specifically it is univ if 1 ∈ s, else empty.

Русский

Пусть s ⊆ β. Тогда предобраз константного отображения 1: α → β равен все множество, если 1 ∈ s, иначе пустое.

LaTeX

$$$ (1 : \alpha \to β)^{-1} s = \begin{cases} \operatorname{Set.univ}, & (1 : β) ∈ s \\ \varnothing, & \text{иначе} \end{cases} $$$

Lean4

@[to_additive]
theorem preimage_one {α β : Type*} [One β] (s : Set β) [Decidable ((1 : β) ∈ s)] :
    (1 : α → β) ⁻¹' s = if (1 : β) ∈ s then Set.univ else ∅ :=
  Set.preimage_const 1 s

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