Commit 2023-01-25 10:47 f58febaf

View on Github →

feat: missing API lemmas about the prod instance in Order/CompleteLattice (#1369) This adds lemmas about how fst, snd, and swap interact with supₛ and infₛ. Manual port of a mathlib PR by @eric-wieser

Estimated changes

added theorem Prod.fst_infᵢ
added theorem Prod.fst_infₛ
added theorem Prod.fst_supᵢ
added theorem Prod.fst_supₛ
added theorem Prod.infᵢ_mk
added theorem Prod.snd_infᵢ
added theorem Prod.snd_infₛ
added theorem Prod.snd_supᵢ
added theorem Prod.snd_supₛ
added theorem Prod.supᵢ_mk
added theorem Prod.swap_infᵢ
added theorem Prod.swap_infₛ
added theorem Prod.swap_supᵢ
added theorem Prod.swap_supₛ
added theorem Sup_prod
added theorem infₛ_Prod