rfl

Mathlib.Analysis.Convex.Extreme

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

English

Another form of reflexivity for IsExtreme: rfl version.

Русский

Еще одна форма рефлексивности IsExtreme.

LaTeX

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

Lean4

protected theorem rfl : IsExtreme 𝕜 A A :=
  IsExtreme.refl 𝕜 A

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

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

Разделы

Аффилиация

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