basisSets_neg — Mathlib

English

For any U in the basis, there exists a basis set V that lies inside the preimage of U under negation.

Русский

Для любого U ∈ p.basisSets существует V ∈ p.basisSets, такой что V ⊆ (−)^{-1}(U).

LaTeX

$$∃ V ∈ p.basisSets, V ⊆ (fun x : E => -x)^{-1} U$$

Lean4

theorem basisSets_neg (U) (hU' : U ∈ p.basisSets) : ∃ V ∈ p.basisSets, V ⊆ (fun x : E => -x) ⁻¹' U :=
  by
  rcases p.basisSets_iff.mp hU' with ⟨s, r, _, hU⟩
  rw [hU, neg_preimage, neg_ball (s.sup p), neg_zero]
  exact ⟨U, hU', Eq.subset hU⟩

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