disjoint_biUnion_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem disjoint_biUnion_left (s : Finset α) (f : α → Finset β) (t : Finset β) :
    Disjoint (s.biUnion f) t ↔ ∀ i ∈ s, Disjoint (f i) t := by
  classical
  refine s.induction ?_ ?_
  · simp only [forall_mem_empty_iff, biUnion_empty, disjoint_empty_left]
  · intro i s his ih
    simp only [disjoint_union_left, biUnion_insert, forall_mem_insert, ih]

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