English
Let α, β be partially ordered sets with infimum operations. Then inf over the product s ×ˢ t of the map Prod.map f g equals the pair (inf s f, inf t g).
Русский
Пусть α и β частично упорядочены с операциями inf; тогда inf над произведением s ×ˢ t от отображения Prod.map f g равен паре (inf s f, inf t g).
LaTeX
$$inf (s ×ˢ t) (Prod.map f g) = (inf s f, inf t g)$$
Lean4
@[simp]
theorem sup_prodMap (hs : s.Nonempty) (ht : t.Nonempty) (f : ι → α) (g : κ → β) :
sup (s ×ˢ t) (Prod.map f g) = (sup s f, sup t g) :=
eq_of_forall_ge_iff fun i ↦ by
obtain ⟨a, ha⟩ := hs
obtain ⟨b, hb⟩ := ht
simp only [Prod.map, Finset.sup_le_iff, mem_product, and_imp, Prod.forall, Prod.le_def]
exact ⟨fun h ↦ ⟨fun i hi ↦ (h _ _ hi hb).1, fun j hj ↦ (h _ _ ha hj).2⟩, by simp_all⟩
