isGLB_prod — Mathlib

English

IsGLB of a set of pairs equals pair of IsGLBs of its projections (dual form).

Русский

Наименьшее нижнее ограничение множества пар эквивалентно парам из нижних ограничений проекций (двойственная формула).

LaTeX

$$$ \\IsGLB s p \\iff IsGLB(\\mathrm{Set.image Prod.fst s}) p.1 \\land IsGLB(\\mathrm{Set.image Prod.snd s}) p.2 $$$

Lean4

theorem isGLB_prod {s : Set (α × β)} (p : α × β) : IsGLB s p ↔ IsGLB (Prod.fst '' s) p.1 ∧ IsGLB (Prod.snd '' s) p.2 :=
  @isLUB_prod αᵒᵈ βᵒᵈ _ _ _ _

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