instInf — Mathlib

English

In the lattice of closed submodules of M over R, the meet (greatest lower bound) of two closed submodules s and t is their intersection s ∩ t; in particular, this intersection is itself a closed submodule.

Русский

В решётке замкнутых подмодулей M над R meet двух подмодулей s и t равен их пересечению s ∩ t; пересечение является замкнутым подмодулем.

LaTeX

$$$s \wedge t = s \cap t$$$

Lean4

instance instInf : Min (ClosedSubmodule R M) where min s t := ⟨s ⊓ t, s.isClosed.inter t.isClosed⟩

Похожие утверждения