refl

Mathlib.Analysis.Convex.Extreme

URI: https://scilib.ai/kg/mathlib#IsExtreme.refl

English

The relation IsExtreme is reflexive: any set A is extreme in itself.

Русский

Отношение IsExtreme рефлексивно: любоя множество является крайним в себе.

LaTeX

$$$$ IsExtreme\ 𝕜\ A\ A. $$$$

Lean4

@[refl]
protected theorem refl (A : Set E) : IsExtreme 𝕜 A A :=
  ⟨Subset.rfl, fun _ hx₁A _ _ _ _ _ ↦ hx₁A⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru