biUnion_le — Mathlib

English

If π1 = π2 and ∀ J ∈ π1, πi1 J = πi2 J, then π1.biUnion πi1 = π2.biUnion πi2.

Русский

Если π1 = π2 и для всех J ∈ π1 выполняется πi1 J = πi2 J, тогда π1.biUnion πi1 = π2.biUnion πi2.

LaTeX

$$Eq π₁ π₂ → (∀ J ∈ π₁, πi₁ J = πi₂ J) → Eq (π₁.biUnion πi₁) (π₂.biUnion πi₂)$$

Lean4

theorem biUnion_le (πi : ∀ J, Prepartition J) : π.biUnion πi ≤ π := fun _ hJ =>
  let ⟨J', hJ', hJ⟩ := π.mem_biUnion.1 hJ
  ⟨J', hJ', (πi J').le_of_mem hJ⟩

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