maximal_maximal — Mathlib

English

The element x being maximal with respect to Maximal P is equivalent to x being maximal with respect to P.

Русский

Элемент x максимален относительно Maximal P тогда и только тогда, когда он максимален относительно P.

LaTeX

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

Lean4

@[simp]
theorem maximal_maximal : Maximal (Maximal P) x ↔ Maximal P x :=
  minimal_minimal (α := αᵒᵈ)

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