isExposed — Mathlib

English

For any A and a linear functional l, the pair (A, l.toExposed A) is exposed; i.e., l induces an exposed subset of A.

Русский

Для любых A и линейного функционала l пара (A, l.toExposed A) экспонирована; тож к функционал l задаёт экспонированное подмножество A.

LaTeX

$$$\\mathrm{IsExposed}\\ 𝕜\\ A\\ (l.toExposed\\ A).$$$

Lean4

theorem isExposed : IsExposed 𝕜 A (l.toExposed A) := fun _ => ⟨l, rfl⟩

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