maximal_iff_forall_ssuperset — Mathlib

English

In Set, Maximal P s holds iff P s and for all t ∈ Set, if s ⊂ t then not P t.

Русский

В Set, Maximal P s выполняется тогда и только тогда, когда P s и для каждого t, если s ⊂ t, то не P t.

LaTeX

$$$$ \\text{Maximal } P s \\iff P s \\land \\forall t\\,(s \\subset t \\to \\lnot P t). $$$$

Lean4

theorem maximal_iff_forall_ssuperset : Maximal P s ↔ P s ∧ ∀ ⦃t⦄, s ⊂ t → ¬P t :=
  maximal_iff_forall_gt

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