prod — Mathlib

English

The product of two filters f and g with realizers F and G has a realizer given by the comap-construction on the product filter, followed by taking inf over the realizers.

Русский

Произведение фильтров f и g с реализаторами F и G имеет реализатор, получаемый через конструкцию comap на произведение фильтров и взятие inf на реализаторах.

LaTeX

$$$\\text{Realizer}(f \\times g) = (F.comap _).inf (G.comap _)$$$

Lean4

/-- Construct a realizer for the product of filters -/
protected def prod {f g : Filter α} (F : f.Realizer) (G : g.Realizer) : (f ×ˢ g).Realizer :=
  (F.comap _).inf (G.comap _)

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