English
The equality of coercions for iInf, with simp attributes.
Русский
Свойство совпадения приведения для iInf со свойством simp.
LaTeX
$$$\\text{(coe}_iInf) = \\text{(coe}_iInf}$$$
Lean4
/-- subsemigroups of a monoid form a complete lattice. -/
@[to_additive /-- The `AddSubsemigroup`s of an `AddMonoid` form a complete lattice. -/
]
instance : CompleteLattice (Subsemigroup M) :=
{
completeLatticeOfInf (Subsemigroup M) fun _ =>
IsGLB.of_image SetLike.coe_subset_coe isGLB_biInf with
le := (· ≤ ·)
lt := (· < ·)
bot := ⊥
bot_le := fun _ _ hx => (notMem_bot hx).elim
top := ⊤
le_top := fun _ x _ => mem_top x
inf := (· ⊓ ·)
sInf := InfSet.sInf
le_inf := fun _ _ _ ha hb _ hx => ⟨ha hx, hb hx⟩
inf_le_left := fun _ _ _ => And.left
inf_le_right := fun _ _ _ => And.right }
