mk_iUnion_le — Mathlib

English

For a family f: ι → Set α, the union is bounded by the index cardinality times the supremum of the cardinals of the members: |⋃_i f(i)| ≤ |ι| · sup_i |f(i)|.

Русский

Для семейства f: ι → Set α объединение ограничено произведением кардинальности индекса и верхней гранью кардиналий элементов: |⋃_i f(i)| ≤ |ι| · sup_i |f(i)|.

LaTeX

$$$\\left|\\bigcup_{i} f(i)\\right| \\le |\\iota| \\cdot \\sup_{i} |f(i)|$$$

Lean4

theorem mk_iUnion_le {α ι : Type u} (f : ι → Set α) : #(⋃ i, f i) ≤ #ι * ⨆ i, #(f i) :=
  mk_iUnion_le_sum_mk.trans (sum_le_iSup _)

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