prod_same_eq — Mathlib

English

The product of a filter with itself equals the lift' of the diagonal product: f ×ˢ f = f.lift' (t ×ˢ t).

Русский

Произведение фильтра с самим собой равно подъему по диагональному произведению: f ×ˢ f = f.lift' (t ×ˢ t).

LaTeX

$$$f \\timesˢ f = f.lift' (\\lambda t. t \\timesˢ t)$$$

Lean4

theorem prod_same_eq : f ×ˢ f = f.lift' fun t : Set α => t ×ˢ t :=
  f.basis_sets.prod_self.eq_biInf

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