disjointedRec — Mathlib

English

If d has pairwise disjointness and partialSups d = partialSups f, then d = disjointed f.

Русский

Если d имеет попарочную несовместимость и partialSups d = partialSups f, то d = disjointed f.

LaTeX

$$$\forall f,d:\ (\forall i

Lean4

/-- An induction principle for `disjointed`. To prove something about `disjointed f i`, it's
enough to prove it for `f i` and being able to extend through diffs.
-/
theorem disjointedRec {f : ι → α} {p : α → Prop} (hdiff : ∀ ⦃t i⦄, p t → p (t \ f i)) :
    ∀ ⦃i⦄, p (f i) → p (disjointed f i) := by
  classical
  intro i hpi
  rw [disjointed]
  suffices ∀ (s : Finset ι), p (f i \ s.sup f) from this _
  intro s
  induction s using Finset.induction with
  | empty => simpa only [sup_empty, sdiff_bot] using hpi
  | insert _ _ ht IH =>
    rw [sup_insert, sup_comm, ← sdiff_sdiff]
    exact hdiff IH

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