basisSets_iff — Mathlib

English

For any Finite index i and radius r > 0, the ball (sup p) ball around 0 with radius r belongs to the basisSets.

Русский

Для любого финитного множества индексов i и радиуса r>0 шар вокруг 0 с радиусом r принадлежит к basisSets.

LaTeX

$$theorem basisSets_mem (i : Finset ι) {r : ℝ} (hr : 0 < r) : (i.sup p).ball 0 r ∈ p.basisSets$$

Lean4

theorem basisSets_iff {U : Set E} : U ∈ p.basisSets ↔ ∃ (i : Finset ι) (r : ℝ), 0 < r ∧ U = ball (i.sup p) 0 r := by
  simp only [basisSets, mem_iUnion, exists_prop, mem_singleton_iff]

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