English
InfClosure provides a closure operator on sets of a join-semilattice that generates a set closed under finite infima.
Русский
InfClosure задаёт замыкание по конечным inf-и на множестве α с полугруппой, оснащённой операцией инфима (meet).
LaTeX
$$$\\operatorname{InfClosed}(\\operatorname{infClosure}(s))$$$
Lean4
/-- Every set in a join-semilattice generates a set closed under join. -/
@[simps! isClosed]
def infClosure : ClosureOperator (Set α) :=
ClosureOperator.ofPred (fun s ↦ {a | ∃ (t : Finset α) (ht : t.Nonempty), ↑t ⊆ s ∧ t.inf' ht id = a}) InfClosed
(fun s a ha ↦ ⟨{ a }, singleton_nonempty _, by simpa⟩)
(by
classical
rintro s _ ⟨t, ht, hts, rfl⟩ _ ⟨u, hu, hus, rfl⟩
refine ⟨_, ht.mono subset_union_left, ?_, inf'_union ht hu _⟩
rw [coe_union]
exact Set.union_subset hts hus)
(by rintro s₁ s₂ hs h₂ _ ⟨t, ht, hts, rfl⟩; exact h₂.finsetInf'_mem ht fun i hi ↦ hs <| hts hi)
