mulIndicator_const_preimage — Mathlib

English

The preimage under a constant-indicator of a set s belongs to a four-element family {univ, U, U^c, ∅}.

Русский

Предобраз константного индикатора от множества s принадлежит четырёхэлементному семейству {univ, U, U^c, ∅}.

LaTeX

$$$(U.mulIndicator (\\lambda _ => a))^{-1} s ∈ ({\\text{univ}}, {U}, {U^c}, {∅})$$$

Lean4

@[to_additive]
theorem mulIndicator_const_preimage (U : Set α) (s : Set M) (a : M) :
    (U.mulIndicator fun _ => a) ⁻¹' s ∈ ({Set.univ, U, Uᶜ, ∅} : Set (Set α)) := by
  classical
  rw [mulIndicator_const_preimage_eq_union]
  split_ifs <;> simp

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