inf — Mathlib

English

If f and g are maximal with respect to l at a, then the infimum of f and g is also maximal at a.

Русский

Если f и g максимальны относительно l в a, то f ∧ g достигает максимума в a.

LaTeX

$$$\\mathrm{IsMaxFilter}(f,l,a) \\land \\mathrm{IsMaxFilter}(g,l,a) \\Rightarrow \\mathrm{IsMaxFilter}(\\lambda x. f(x) \\otimes g(x), l, a)$$$

Lean4

theorem inf (hf : IsMaxFilter f l a) (hg : IsMaxFilter g l a) : IsMaxFilter (fun x => f x ⊓ g x) l a :=
  show IsMaxFilter (fun x => f x ⊓ g x) l a from hf.bicomp_mono (fun _x _x' hx _y _y' hy => inf_le_inf hx hy) hg

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