minimal_subset_iff — Mathlib

English

For P : Set α → Prop and s, Minimal P s, we have Minimal P s if and only if P s and ∀ t, P t → t ⊆ s → s = t.

Русский

Для P : Set α → Prop и s, Minimal P s имеет место тогда и только тогда, когда P s и для всех t, если P t, и t ⊆ s, то s = t.

LaTeX

$$$$ Minimal P s \\iff P s \\land \\forall t\\,(P t \\to t \\subseteq s \\to s = t). $$$$

Lean4

theorem minimal_subset_iff : Minimal P s ↔ P s ∧ ∀ ⦃t⦄, P t → t ⊆ s → s = t :=
  _root_.minimal_iff

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