sInf_sup_sInf — Mathlib

English

The join of two Infimums equals the Infimum over the product set of the coordinatewise join: sInf s ⊔ sInf t = ⨅ p ∈ s ×ˢ t, (p.1 ⊔ p.2).

Русский

Объединение двух инфимумов равно инфимуму над произведением множеств с координатным объединением.

LaTeX

$$$\operatorname{sInf} s \lor \operatorname{sInf} t = \inf_{p \in s \times^{\!} t} (p_1 \lor p_2)$$$

Lean4

theorem sInf_sup_sInf : sInf s ⊔ sInf t = ⨅ p ∈ s ×ˢ t, (p : α × α).1 ⊔ p.2 :=
  @sSup_inf_sSup αᵒᵈ _ _ _

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