preimage_boolIndicator — Mathlib

English

For any t ⊆ {true,false}, the preimage under the indicator is always one of {univ}, s, sᶜ, or ∅.

Русский

Для любого t ⊆ {true,false} предобраз индикатора всегда равен одному из {всего}, s, sᶜ или ∅.

LaTeX

$$$s.boolIndicator^{-1} t \\in \\{\\mathrm{univ}, s, s^{\\mathrm{c}}, \\emptyset\\}$$$

Lean4

theorem preimage_boolIndicator (t : Set Bool) :
    s.boolIndicator ⁻¹' t = univ ∨ s.boolIndicator ⁻¹' t = s ∨ s.boolIndicator ⁻¹' t = sᶜ ∨ s.boolIndicator ⁻¹' t = ∅ :=
  by
  simp only [preimage_boolIndicator_eq_union]
  split_ifs <;> simp [s.union_compl_self]

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