minimalFor_id

Mathlib.Order.Minimal

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

English

Reiteration: For any i, j, f, the maximal-for-equality condition holds iff i = j.

Русский

Повторно: для любых i, j, f условие максимального для равенства держится тогда и только тогда, когда i = j.

LaTeX

$$$ \text{MaximalFor}(x \mapsto x = j)\ f\ i \iff i = j $$$

Lean4

@[simp]
theorem minimalFor_id : MinimalFor P id x ↔ Minimal P x :=
  .rfl

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

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

Разделы

Аффилиация

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