disjoint_sup_right — Mathlib

English

Disjoint a with s.sup f iff for all i ∈ s, Disjoint a (f i).

Русский

Пусть a дисъюнктно не пересекается с объединением s над f, тогда это эквивалентно тому, что для всех i ∈ s, Disjoint a (f i).

LaTeX

$$$ Disjoint a (s.\\sup f) \\iff \\forall i, i \\in s \\to Disjoint a (f i) $$$

Lean4

protected theorem disjoint_sup_right : Disjoint a (s.sup f) ↔ ∀ ⦃i⦄, i ∈ s → Disjoint a (f i) := by
  simp only [disjoint_iff, sup_inf_distrib_left, Finset.sup_eq_bot_iff]

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