minimal_iff_forall_diff_singleton

English

In Set, Minimal P s is equivalent to P s and for all x ∈ s, not P(s \\ { x }).

Русский

В Set, Minimal P s эквивалентно P s и для всех x ∈ s: не P (s \\ { x }).

LaTeX

$$$$ \\text{Minimal } P s \\iff P s \\land \\forall x\\in s, \\lnot P\\,(s \\setminus \\{x\\}). $$$$

Lean4

theorem minimal_iff_forall_diff_singleton (hP : ∀ ⦃s t⦄, P t → t ⊆ s → P s) :
    Minimal P s ↔ P s ∧ ∀ x ∈ s, ¬P (s \ { x }) :=
  ⟨fun h ↦ ⟨h.1, fun _ hx hP ↦ h.notMem_of_prop_diff_singleton hP hx⟩, fun h ↦
    ⟨h.1, fun _ ht hts x hxs ↦ by_contra fun hxt ↦ h.2 x hxs (hP ht <| subset_diff_singleton hts hxt)⟩⟩

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