English
An element x lies in the infimum sInf S iff x lies in every p ∈ S.
Русский
Элемент x принадлежит наименьшему элементу infimum sInf S тогда и только тогда, когда x принадлежит каждому p ∈ S.
LaTeX
$$$x \in \mathrm{sInf}(S) \iff \forall p \in S,\ x \in p$$$
Lean4
instance completeLattice : CompleteLattice (Submodule R M) :=
{ (inferInstance : OrderTop (Submodule R M)),
(inferInstance : OrderBot
(Submodule R M)) with
sup := fun a b ↦ sInf {x | a ≤ x ∧ b ≤ x}
le_sup_left := fun _ _ ↦ le_sInf' fun _ ⟨h, _⟩ ↦ h
le_sup_right := fun _ _ ↦ le_sInf' fun _ ⟨_, h⟩ ↦ h
sup_le := fun _ _ _ h₁ h₂ ↦ sInf_le' ⟨h₁, h₂⟩
inf := (· ⊓ ·)
le_inf := fun _ _ _ ↦ Set.subset_inter
inf_le_left := fun _ _ ↦ Set.inter_subset_left
inf_le_right := fun _ _ ↦ Set.inter_subset_right
sSup S := sInf {sm | ∀ s ∈ S, s ≤ sm}
le_sSup := fun _ _ hs ↦ le_sInf' fun _ hq ↦ by exact hq _ hs
sSup_le := fun _ _ hs ↦ sInf_le' hs
le_sInf := fun _ _ ↦ le_sInf'
sInf_le := fun _ _ ↦ sInf_le' }
