Theorem Finset.coe_sup_of_nonempty

Modification history

2026-06-27 13:04
Mathlib/Data/Finset/Lattice/Fold.lean
feat(Topology/MetricSpace): the L^p direct sum of metric spaces (#40212) …
Modified Finset.coe_sup_of_nonemptyView on Github →
2023-01-17 10:40
Mathlib/Data/Finset/Lattice.lean
feat: port Data.Finset.Lattice (#1606)
Added Finset.coe_sup_of_nonemptyView on Github →