English
For semilattice with sup, the upper closure distributes over sups: upperClosure(s ⊻ t) = upperClosure(s) ⊔ upperClosure(t).
Русский
Для полупорядованной сверху с объединением верхних множеств верхнее замыкание распределяется над супермножествами: верхнее замыкание (s ⊻ t) равно верхнему замыканию s плюс верхнему замыканию t.
LaTeX
$$$\\text{upperClosure}(s \\⊻ t) = \\text{upperClosure}(s) \\sqcup \\text{upperClosure}(t)$$$
Lean4
@[simp]
theorem upperClosure_sups [SemilatticeSup α] (s t : Set α) : upperClosure (s ⊻ t) = upperClosure s ⊔ upperClosure t :=
by
ext a
simp only [SetLike.mem_coe, mem_upperClosure, Set.mem_sups, UpperSet.coe_sup, Set.mem_inter_iff]
constructor
· rintro ⟨_, ⟨b, hb, c, hc, rfl⟩, ha⟩
exact ⟨⟨b, hb, le_sup_left.trans ha⟩, c, hc, le_sup_right.trans ha⟩
· rintro ⟨⟨b, hb, hab⟩, c, hc, hac⟩
exact ⟨_, ⟨b, hb, c, hc, rfl⟩, sup_le hab hac⟩
