biUnion — Mathlib

English

If π is a partition and each πi(J) is a partition for all J ∈ π, then the biUnion partition π.biUnion πi is a partition.

Русский

Если π — разбиение, и для каждого J ∈ π множество πi(J) образует разбиение, то объединение по частям образует разбиение.

LaTeX

$$$\\pi.I sPartition \\Rightarrow (\\forall J, J \\in \\pi \\rightarrow (\\pi_i J).IsPartition) \\Rightarrow (\\pi.biUnion \\pi_i).IsPartition.$$$

Lean4

protected theorem biUnion (h : IsPartition π) (hi : ∀ J ∈ π, IsPartition (πi J)) : IsPartition (π.biUnion πi) :=
  fun x hx =>
  let ⟨J, hJ, hxi⟩ := h x hx
  let ⟨Ji, hJi, hx⟩ := hi J hJ x hxi
  ⟨Ji, π.mem_biUnion.2 ⟨J, hJ, hJi⟩, hx⟩

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