instMin — Mathlib

English

For filtrations f and g, the underlying function of their infimum is the pointwise infimum of the underlying functions: coe(f ⊓ g) = coe(f) ⊓ coe(g).

Русский

Для фильтраций f и g соответствующая отображение их Infimum равно точечному пересечению: коэрционация lf(f ⊓ g) = lf(f) ⊓ lf(g).

LaTeX

$$$\\operatorname{coe}(f \\inf g) = \\operatorname{coe}(f) \\inf \\operatorname{coe}(g).$$$

Lean4

instance : Min (Filtration ι m) :=
  ⟨fun f g =>
    { seq := fun i => f i ⊓ g i
      mono' := fun _ _ hij => le_inf (inf_le_left.trans (f.mono hij)) (inf_le_right.trans (g.mono hij))
      le' := fun i => inf_le_left.trans (f.le i) }⟩

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