nonneg_of_mem_compactSet — Mathlib

English

The interior of compactSet equals the product of Icc intervals, scaled by expMapBasis.

Русский

Interior(compactSet) равен произведению интервалов Icc, масштабированных через expMapBasis.

LaTeX

$$interior(compactSet K) = Set.Icc(0,1) • expMapBasis'' Set.univ.pi (fun w => if w = w0 then {0} else Set.Icc 0 1)$$

Lean4

theorem nonneg_of_mem_compactSet {x : realSpace K} (hx : x ∈ compactSet K) (w : InfinitePlace K) : 0 ≤ x w :=
  by
  obtain ⟨c, hc, ⟨_, ⟨⟨a, ha, rfl⟩, _, rfl⟩⟩⟩ := hx
  exact mul_nonneg hc.1 (expMapBasis_pos _ _).le

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