prod_eq_inf — Mathlib

English

If f₁ and f₂ have a binary product, then their product equals their infimum: f₁ ⨯ f₂ = f₁ ⊓ f₂.

Русский

Если существуют двоичные произведения подмножеств f₁ и f₂, то их произведение равно их наименьшему: f₁ ⨯ f₂ = f₁ ⊓ f₂.

LaTeX

$$$ (f_1 \\boxtimes f_2) = f_1 \\wedge f_2 $$$

Lean4

theorem prod_eq_inf {A : C} {f₁ f₂ : Subobject A} [HasBinaryProduct f₁ f₂] : (f₁ ⨯ f₂) = f₁ ⊓ f₂ :=
  by
  apply le_antisymm
  · refine le_inf _ _ _ (Limits.prod.fst.le) (Limits.prod.snd.le)
  · apply leOfHom
    exact prod.lift (inf_le_left _ _).hom (inf_le_right _ _).hom

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