minimal_iff_forall_ssubset — Mathlib

English

Set.minimal_iff_forall_ssubset: Minimal P s iff P s and ∀ t, P t → t ⊂ s → Not (P t).

Русский

Set.minimal_iff_forall_ssubset: Minimal P s эквивалентно P s и для всякого t, если P t, и t ⊂ s, то ¬P t.

LaTeX

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

Lean4

theorem minimal_iff_forall_ssubset : Minimal P s ↔ P s ∧ ∀ ⦃t⦄, t ⊂ s → ¬P t :=
  minimal_iff_forall_lt

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