mul_closure_one_eq — Mathlib

English

For any measurable set s in G, s * closure{1} = s.

Русский

Для любого измеримого множества s в G выполняется s ⋅ closure{1} = s.

LaTeX

$$$\text{MeasurableSet}(s) \Rightarrow s \cdot \overline{\{1\}} = s$$$

Lean4

@[to_additive]
theorem _root_.MeasurableSet.mul_closure_one_eq {s : Set G} (hs : MeasurableSet s) : s * (closure { 1 } : Set G) = s :=
  by
  induction s, hs using MeasurableSet.induction_on_open with
  | isOpen U hU => exact hU.mul_closure_one_eq
  | compl t _ iht => exact compl_mul_closure_one_eq_iff.2 iht
  | iUnion f _ _ ihf => simp_rw [iUnion_mul f, ihf]

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