indicator_one_preimage — Mathlib

English

For any U ⊆ α and s ⊆ M (with zeros allowed), the preimage under U.indicator 1 of s lies in a finite four-element family.

Русский

Для любой U ⊆ α и s ⊆ M (ноль допускается) предобраз U.indicator 1 от s принадлежит четырехэлементному семейству.

LaTeX

$$U.indicator 1 ^{-1} s ∈ ({Set.univ, U, U^c, ∅} : Set (Set α))$$

Lean4

theorem indicator_one_preimage [Zero M] (U : Set α) (s : Set M) :
    U.indicator 1 ⁻¹' s ∈ ({Set.univ, U, Uᶜ, ∅} : Set (Set α)) :=
  indicator_const_preimage _ _ 1

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