English
For semilattice with inf, the lower closure distributes over inf: lowerClosure(s ⊼ t) = lowerClosure(s) ⊓ lowerClosure(t).
Русский
Для полупорядованной частичной упорядованности инф распределяется через нижнее замыкание: нижнее замыкание (s ⊼ t) равно нижнему замыканию s ∧ нижнему замыканию t.
LaTeX
$$$\\text{lowerClosure}(s \\⊼ t) = \\text{lowerClosure}(s) \\sqcap \\text{lowerClosure}(t)$$$
Lean4
@[simp]
theorem lowerClosure_infs [SemilatticeInf α] (s t : Set α) : lowerClosure (s ⊼ t) = lowerClosure s ⊓ lowerClosure t :=
by
ext a
simp only [SetLike.mem_coe, mem_lowerClosure, Set.mem_infs]
constructor
· rintro ⟨_, ⟨b, hb, c, hc, rfl⟩, ha⟩
exact ⟨⟨b, hb, ha.trans inf_le_left⟩, c, hc, ha.trans inf_le_right⟩
· rintro ⟨⟨b, hb, hab⟩, c, hc, hac⟩
exact ⟨_, ⟨b, hb, c, hc, rfl⟩, le_inf hab hac⟩
