plusPart — Mathlib

English

The plusPart of a subset A of the mixed space is the subset of A consisting of elements that are strictly positive at every real place: plusPart(A) = A ∩ { x | ∀ w, 0 < x.1 w }.

Русский

Часть плюс множества A состоит из таких элементов A, которые положительны во всех вещественных местах: plusPart(A) = A ∩ { x | ∀ w, 0 < x_1(w) }.

LaTeX

$$plusPart(A) = A \cap { x ∈ \text{mixedSpace}(K) \mid \forall w, 0 < x_1(w) }$$

Lean4

/-- The `plusPart` of a subset `A` of the `mixedSpace` is the set of points in `A` that are
positive at all real places. -/
abbrev plusPart : Set (mixedSpace K) :=
  A ∩ {x | ∀ w, 0 < x.1 w}

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