mk_sUnion_le — Mathlib

English

For A a set of sets, the cardinality of the sUnion is bounded by the product of |A| and the supremum of the cardinalities of its members: |⋃₀ A| ≤ |A| · sup_{S∈A} |S|.

Русский

Для множества A множеств справедливо: |⋃₀ A| ≤ |A| · sup_{S∈A} |S|.

LaTeX

$$$\\left|\\bigcup A\\right| \\le |A| \\cdot \\sup_{S\\in A} |S|$$

Lean4

theorem mk_sUnion_le {α : Type u} (A : Set (Set α)) : #(⋃₀ A) ≤ #A * ⨆ s : A, #s :=
  by
  rw [sUnion_eq_iUnion]
  apply mk_iUnion_le

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