Theorems · Theorem · order theory

Set.iUnion_pi_of_monotone

∀ {ι : Type u_1} {ι' : Type u_2} [inst : LinearOrder ι'] [Nonempty ι'] {α : ι → Type u_3} {I : Set ι}
  {s : (i : ι) → ι' → Set (α i)},
  I.Finite → (∀ i ∈ I, Monotone (s i)) → (⋃ j, I.pi fun i => s i j) = I.pi fun i => ⋃ j, s i j

Defined in

Mathlib.Data.Set.Finite.Lattice

Cited by

1 results in Mathlib

Foundations

Depth 71 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

LinearOrderNonempty