instMax — Mathlib

English

The supremum (join) of two I-filtrations is again an I-filtration, with N-component equal to the join of the N-components: (F ⊔ F').N = F.N ⊔ F'.N and compatible N’s with i.

Русский

Наибольшее объединение двух I-фильтраций вновь является I-фильтрацией; его компонент N равен объединению компонент N: (F ⊔ F').N = F.N ⊔ F'.N.

LaTeX

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

Lean4

/-- The `sup` of two `I.Filtration`s is an `I.Filtration`. -/
instance : Max (I.Filtration M) :=
  ⟨fun F F' =>
    ⟨F.N ⊔ F'.N, fun i => sup_le_sup (F.mono i) (F'.mono i), fun i =>
      (Submodule.smul_sup _ _ _).trans_le <| sup_le_sup (F.smul_le i) (F'.smul_le i)⟩⟩

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