Conditional statements

Stream: mathlib4

[Daniel Weber]

Would conditional results from set theory be on topic for Mathlib? Formalizing some statements which are independent of ZFC and showing implications between them

[Violeta Hernández]

I've always thought it'd be fun to have a file with consequences of CH/GCH, though perhaps there's not too many of them.