interior — Mathlib

English

The interior of a balanced set is balanced provided it contains the origin.

Русский

Interior сбалансированного множества остается сбалансированным, если он содержит нуль.

LaTeX

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

Lean4

/-- The interior of a balanced set is balanced if it contains the origin. -/
protected theorem interior (hA : Balanced 𝕜 A) (h : (0 : E) ∈ interior A) : Balanced 𝕜 (interior A) :=
  by
  rw [← insert_eq_self.2 h]
  exact hA.zero_insert_interior

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