sup — Mathlib

English

If f and g are both minimal, their supremum f x ⊔ g x is also minimal on the same index set.

Русский

Если f и g минимальны, их числительное объединение f x ⊔ g x также минимально на том же множестве.

LaTeX

$$$hf : IsMinFilter f l a \; hg : IsMinFilter g l a \Rightarrow IsMinFilter (fun x => f x ⊔ g x) l a$$$

Lean4

theorem sup (hf : IsMinFilter f l a) (hg : IsMinFilter g l a) : IsMinFilter (fun x => f x ⊔ g x) l a :=
  show IsMinFilter (fun x => f x ⊔ g x) l a from hf.bicomp_mono (fun _x _x' hx _y _y' hy => sup_le_sup hx hy) hg

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