English
Subrings of a ring form a complete lattice under inclusion, with bottom ⊥ and top ⊤, and infimum given by intersection.
Русский
Подкольца кольца образуют полную решётку по включению, нижнее ⊥ и верхнее ⊤, а инфимум равен пересечению.
LaTeX
$$$\\text{CompleteLattice} (\\text{Subring } R)$$$
Lean4
/-- Subrings of a ring form a complete lattice. -/
instance : CompleteLattice (Subring R) :=
{
completeLatticeOfInf (Subring R) fun _ =>
IsGLB.of_image SetLike.coe_subset_coe isGLB_biInf with
bot := ⊥
bot_le := fun s _x hx =>
let ⟨n, hn⟩ := mem_bot.1 hx
hn ▸ intCast_mem s n
top := ⊤
le_top := fun _s _x _hx => trivial
inf := (· ⊓ ·)
inf_le_left := fun _s _t _x => And.left
inf_le_right := fun _s _t _x => And.right
le_inf := fun _s _t₁ _t₂ h₁ h₂ _x hx => ⟨h₁ hx, h₂ hx⟩ }
