mk_biUnion_le_lift — Mathlib

English

Let A: ι → Set α and s ⊆ ι. Then lifting the cardinality bound for the biUnion holds: lift(|⋃ x∈s, A x|) ≤ lift(|s|) · ⨆ x : s, lift(|A x.1|).

Русский

Пусть A: ι → Set α и s ⊆ ι. Тогда выполняется подъем ограничение по биобъединению: lift(|⋃ x∈s, A x|) ≤ lift(|s|) · ⨆ x ∈ s, lift(|A(x)|).

LaTeX

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

Lean4

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

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