minimal_iff_forall_diff_singleton

English

Let Finset α be equipped with a predicate P: Finset α → Prop which is upward closed under removing elements (i.e., if P(s) then P(s.erase x) for x ∈ s). Then Minimal P s holds iff P(s) and for all x ∈ s, ¬P(s.erase x).

Русский

Пусть P: Finset α → Prop возрастает при удалении элементов; тогда минимальность P(s) эквивалентна: P(s) и для каждого x ∈ s, ¬P(s.erase x).

LaTeX

$$$$\\text{Minimal } P(s) \\iff P(s) \\land \\forall x \\in s, \\neg 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.erase x)
    where
  mp h := ⟨h.prop, fun x hxs hx ↦ by simpa using h.le_of_le hx (erase_subset _ _) hxs⟩
  mpr h := ⟨h.1, fun t ht hts x hxs ↦ by_contra fun hxt ↦ h.2 x hxs <| hP ht (subset_erase.2 ⟨hts, hxt⟩)⟩

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