mk_biUnion_le — Mathlib

English

Let A: ι → Set α and s ⊆ ι. Then #(⋃ x∈s, A x) ≤ #s · ⨆ x : s, #(A x.1).

Русский

Пусть A: ι → Set α и s ⊆ ι. Тогда #(⋃ x∈s, A x) ≤ #s · ⨆ x ∈ s, #(A x).

LaTeX

$$$\\left|\\bigcup_{x\\in s} A(x)\\right| \\le |s| \\cdot \\sup_{x\\in s} |A(x)|$$

Lean4

theorem mk_biUnion_le {ι α : Type u} (A : ι → Set α) (s : Set ι) : #(⋃ x ∈ s, A x) ≤ #s * ⨆ x : s, #(A x.1) :=
  by
  rw [biUnion_eq_iUnion]
  apply mk_iUnion_le

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