instMin — Mathlib

English

The infimum (intersection) of two I-filtrations is an I-filtration with N-component equal to the infimum of the two N-components: (F ⊓ F').N = F.N ⊓ F'.N.

Русский

Пересечение двух I-фильтраций есть I-фильтрация; компонент N равен пересечению: (F ⊓ F').N = F.N ⊓ F'.N.

LaTeX

$$(F ⊓ F').N = F.N ⊓ F'.N$$

Lean4

/-- The `inf` of two `I.Filtration`s is an `I.Filtration`. -/
instance : Min (I.Filtration M) :=
  ⟨fun F F' =>
    ⟨F.N ⊓ F'.N, fun i => inf_le_inf (F.mono i) (F'.mono i), fun i =>
      (smul_inf_le _ _ _).trans <| inf_le_inf (F.smul_le i) (F'.smul_le i)⟩⟩

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