Commit 2022-12-06 00:34 a95b16cb

View on Github →

chore(data/set/constructions): Make has_finite_inter Prop-valued (#17824) has_finite_inter was accidentally defined to be Type-valued, despite only having propositional fields.

Estimated changes

Modified src/data/set/constructions.lean

added theorem has_finite_inter.finite_inter_closure_has_finite_inter

deleted def has_finite_inter.finite_inter_closure_has_finite_inter

modified structure has_finite_inter