zero_insert_interior — Mathlib

English

If A is balanced, then inserting 0 into the interior yields a balanced set.

Русский

Если A сбалансировано, то добавление 0 в interior сохраняет сбалансированность.

LaTeX

$$$\text{Balanced } 𝕜 A \Rightarrow \text{Balanced } 𝕜 (insert 0 (interior A))$$$

Lean4

/-- The union of `{0}` with the interior of a balanced set is balanced. -/
theorem zero_insert_interior (hA : Balanced 𝕜 A) : Balanced 𝕜 (insert 0 (interior A)) :=
  by
  intro a ha
  obtain rfl | h := eq_or_ne a 0
  · rw [zero_smul_set]
    exacts [subset_union_left, ⟨0, Or.inl rfl⟩]
  · rw [← image_smul, image_insert_eq, smul_zero]
    apply insert_subset_insert
    exact ((isOpenMap_smul₀ h).mapsTo_interior <| hA.smul_mem ha).image_subset

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