minimal_minimal

Mathlib.Order.Minimal

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

English

The property Minimal (Minimal P) at x is equivalent to Minimal P at x.

Русский

Свойство Minimal (Minimal P) в точке x эквивалентно Minimal P в x.

LaTeX

$$$\\text{Minimal}(\\text{Minimal } P)\\, x \\iff \\text{Minimal } P\\, x$$$

Lean4

@[simp]
theorem minimal_minimal : Minimal (Minimal P) x ↔ Minimal P x :=
  ⟨fun h ↦ h.prop, fun h ↦ ⟨h, fun _ hy hyx ↦ h.le_of_le hy.prop hyx⟩⟩

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

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

Разделы

Аффилиация

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