coprod_eq_prod_top_sup_top_prod — Mathlib

English

The coprod of f and g equals the supremum (maximum) of f×⊤ and ⊤×g: coprod f g = f ×⊤ ⊔ ⊤ ×⊤ g.

Русский

Копродукт фильтров f и g равен наивысшей границе между f×⊤ и ⊤×g.

LaTeX

$$$ \\operatorname{coprod} f g = f \\times\\! \\top \\; \\sqcup \\; \\top \\times\\! g $$$

Lean4

theorem coprod_eq_prod_top_sup_top_prod (f : Filter α) (g : Filter β) : Filter.coprod f g = f ×ˢ ⊤ ⊔ ⊤ ×ˢ g :=
  by
  rw [prod_top, top_prod]
  rfl

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