sup_mul_inf — Mathlib

English

A lattice structure on Associates α is provided, describing sup and inf operations.

Русский

Для множества Associates α задана структура латтицы с операциями наивысшего и наименьшего.

LaTeX

$$Lattice (Associates α)$$

Lean4

theorem sup_mul_inf (a b : Associates α) : (a ⊔ b) * (a ⊓ b) = a * b :=
  show (a.factors ⊔ b.factors).prod * (a.factors ⊓ b.factors).prod = a * b
    by
    nontriviality α
    refine eq_of_factors_eq_factors ?_
    rw [← prod_add, prod_factors, factors_mul, FactorSet.sup_add_inf_eq_add]

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