maximal_ge_iff

Mathlib.Order.Minimal

URI: https://scilib.ai/kg/mathlib#maximal_ge_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 \le \cdot) x \leftrightarrow y \le x \land \operatorname{IsMax} x $$$

Lean4

@[simp]
theorem maximal_ge_iff : Maximal (y ≤ ·) x ↔ y ≤ x ∧ IsMax x :=
  minimal_le_iff (α := αᵒᵈ)

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

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

Разделы

Аффилиация

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