Commit 2022-11-11 07:33 b1cf06cb

View on Github →

chore: rename and alignment is_empty → isEmpty in lemmas (#571)

Estimated changes

deleted theorem Subtype.is_empty_of_false
added theorem isEmpty_Prop
added theorem isEmpty_iff
added theorem isEmpty_or_nonempty
added theorem isEmpty_pi
added theorem isEmpty_plift
added theorem isEmpty_pprod
added theorem isEmpty_prod
added theorem isEmpty_psigma
added theorem isEmpty_psum
added theorem isEmpty_sigma
added theorem isEmpty_subtype
added theorem isEmpty_sum
added theorem isEmpty_ulift
deleted theorem is_empty_Prop
deleted theorem is_empty_iff
deleted theorem is_empty_or_nonempty
deleted theorem is_empty_pi
deleted theorem is_empty_plift
deleted theorem is_empty_pprod
deleted theorem is_empty_prod
deleted theorem is_empty_psigma
deleted theorem is_empty_psum
deleted theorem is_empty_sigma
deleted theorem is_empty_subtype
deleted theorem is_empty_sum
deleted theorem is_empty_ulift
added theorem not_isEmpty_iff
deleted theorem not_is_empty_iff
deleted theorem not_is_empty_of_nonempty