iUnion_inf — Mathlib

English

The iUnion of the infimum equals the intersection of the iUnions: (π1 ⊓ π2).iUnion = π1.iUnion ∩ π2.iUnion.

Русский

Объединение по iUnion у наихудшего элемента равно пересечению iUnion: (π1 ⊓ π2).iUnion = π1.iUnion ∩ π2.iUnion.

LaTeX

$$$ (\pi_1 \sqcap \pi_2).iUnion = \pi_1.iUnion \cap \pi_2.iUnion. $$$

Lean4

@[simp]
theorem iUnion_inf (π₁ π₂ : Prepartition I) : (π₁ ⊓ π₂).iUnion = π₁.iUnion ∩ π₂.iUnion := by
  simp only [inf_def, iUnion_biUnion, iUnion_restrict, ← iUnion_inter, ← iUnion_def]

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