proposition: Lemma eq_ppsum (F1 F2 : {fset T} -> R) : F1 =1 F2 -> (sup [set x | exists J, x = F1 J] = sup [set x | exists J, x = F2 J])%classic.
proof: Proof. move=> eq_12; congr sup; rewrite predeqE => x. by split=> -[J ->]; exists J. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology