maximal_gt_iff

Mathlib.Order.Minimal

URI: https://scilib.ai/kg/mathlib#maximal_gt_iff

English

Maximal with respect to y < · at x is equivalent to y < x and IsMax x.

Русский

Максимальность по отношению к y < · в точке x эквивалентна y < x и IsMax x.

LaTeX

$$$ \operatorname{Maximal}(y < \cdot) x \leftrightarrow y < x \land \operatorname{IsMax} x $$$

Lean4

@[simp]
theorem maximal_gt_iff : Maximal (y < ·) x ↔ y < x ∧ IsMax x :=
  minimal_lt_iff (α := αᵒᵈ)

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

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

Разделы

Аффилиация

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