disjoint_biUnion_right — Mathlib

English

Disjoint s (t.biUnion f) is equivalent to disjointness of s with each f i: Disjoint s (t.biUnion f) ⇔ ∀ i ∈ t, Disjoint s (f i).

Русский

Пусть Disjoint s (t.biUnion f) эквивалентно дисjointness с каждой f(i): ∀ i ∈ t, Disjoint s (f i).

LaTeX

$$$\\mathrm{Disjoint}(s, t.biUnion f) \\iff \\forall i \\in t, \\mathrm{Disjoint}(s, f(i))$$$

Lean4

theorem disjoint_biUnion_right (s : Finset β) (t : Finset α) (f : α → Finset β) :
    Disjoint s (t.biUnion f) ↔ ∀ i ∈ t, Disjoint s (f i) := by
  simpa only [_root_.disjoint_comm] using disjoint_biUnion_left t f s

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