disjointed_eq_self — Mathlib

English

If for all j<i, Disjoint (f j) (f i), then disjointed f i = f i.

Русский

Если для каждого j<i выполняется Disjoint (f j) (f i), то disjointed f i = f i.

LaTeX

$$$\forall f,i\ (\forall j

Lean4

theorem disjointed_eq_self {f : ι → α} {i : ι} (hf : ∀ j < i, Disjoint (f j) (f i)) : disjointed f i = f i :=
  by
  rw [disjointed_apply, sdiff_eq_left, disjoint_iff, sup_inf_distrib_left,
    sup_congr rfl <| fun j hj ↦ disjoint_iff.mp <| (hf _ (mem_Iio.mp hj)).symm]
  exact
    sup_bot
      _
        /- NB: The original statement for `ι = ℕ` was a `def` and worked for `p : α → Sort*`. I couldn't
        prove the `Sort*` version for general `ι`, but all instances of `disjointedRec` in the library are
        for Prop anyway. -/

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