Theorem Set.image_inf_prod

Modification history

2025-10-07 17:36

Mathlib/Data/Set/Sups.lean

chore(Data): golf entire `equivFunOnFintype_single`, `predAbove_right_zero`, `snoc_zero` and more using `rfl` (#28561)

Modified Set.image_inf_prod View on Github →

2023-03-23 14:35

Mathlib/Data/Set/Sups.lean

feat: port Data.Set.Sups (#2991)

Added Set.image_inf_prod View on Github →