mulIndicator_one_preimage — Mathlib

English

The preimage under t.mulIndicator 1 of s is either universal or empty, depending on whether 1 is in s.

Русский

Предобраз под t.mulIndicator 1 от s либо все пространство, либо пустое, в зависимости от того, принадлежит ли 1 s.

LaTeX

$$$t.mulIndicator 1^{-1} s \\in (\\{\\,\\mathsf{univ}, \\varnothing\\} : Set (Set \\alpha))$$$

Lean4

@[to_additive]
theorem mulIndicator_one_preimage (s : Set M) : t.mulIndicator 1 ⁻¹' s ∈ ({Set.univ, ∅} : Set (Set α)) := by
  classical
  rw [mulIndicator_one', Pi.one_def, Set.preimage_const]
  split_ifs <;> simp

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