exposed_point_def — Mathlib

English

A point x belongs to exposedPoints of A iff the singleton {x} is exposed in A.

Русский

Точка x принадлежит экспонированным точкам A тогда и только тогда, когда {x} экспонировано в A.

LaTeX

$$$$ x \in A.exposedPoints 𝕜 \iff IsExposed 𝕜 A { x }. $$$$

Lean4

theorem exposed_point_def :
    x ∈ A.exposedPoints 𝕜 ↔ x ∈ A ∧ ∃ l : StrongDual 𝕜 E, ∀ y ∈ A, l y ≤ l x ∧ (l x ≤ l y → y = x) :=
  Iff.rfl

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