basisSets_add — Mathlib

English

For any U in the basis, there exists V in the basis such that V + V ⊆ U.

Русский

Для любого U ∈ p.basisSets существует V ∈ p.basisSets с V + V ⊆ U.

LaTeX

$$∃ V ∈ p.basisSets, V + V ⊆ U$$

Lean4

theorem basisSets_add (U) (hU : U ∈ p.basisSets) : ∃ V ∈ p.basisSets, V + V ⊆ U :=
  by
  rcases p.basisSets_iff.mp hU with ⟨s, r, hr, hU⟩
  use (s.sup p).ball 0 (r / 2)
  refine ⟨p.basisSets_mem s (div_pos hr zero_lt_two), ?_⟩
  refine Set.Subset.trans (ball_add_ball_subset (s.sup p) (r / 2) (r / 2) 0 0) ?_
  rw [hU, add_zero, add_halves]

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