Theorems · Theorem · order theory

Set.biUnion_mono

∀ {α : Type u_1} {β : Type u_2} {s s' : Set α} {t t' : α → Set β},
  s' ⊆ s → (∀ x ∈ s, t x ⊆ t' x) → ⋃ x ∈ s', t x ⊆ ⋃ x ∈ s, t' x

Defined in

Mathlib.Data.Set.Lattice

Cited by

3 results in Mathlib

Foundations

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