Read-only archive. Publishing has closed. GitHub

theorem Set.union_subset_iff

theorem Set.union_subset_iff
: ∀ {α : Type u} {s t u : Set α}, s ∪ t ⊆ u ↔ s ⊆ u ∧ t ⊆ u

Published by @sam ·

View source in zpg9xh52

Definitional, with no premises to accept.