Commit 2022-10-24 00:48 6a2d6f50

View on Github →

feat: Port Logic.IsEmpty (#486) Following @semorrison's video

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Logic/Function/Basic.lean

added theorem Function.extend_apply'

Created Mathlib/Logic/IsEmpty.lean

added theorem Function.extend_of_empty

added theorem IsEmpty.exists_iff

added theorem IsEmpty.forall_iff

added theorem Subtype.is_empty_of_false

added def isEmptyElim

added theorem is_empty_Prop

added theorem is_empty_iff

added theorem is_empty_or_nonempty

added theorem is_empty_pi

added theorem is_empty_plift

added theorem is_empty_pprod

added theorem is_empty_prod

added theorem is_empty_psigma

added theorem is_empty_psum

added theorem is_empty_sigma

added theorem is_empty_subtype

added theorem is_empty_sum

added theorem is_empty_ulift

added theorem not_is_empty_iff

added theorem not_is_empty_of_nonempty

added theorem not_nonempty_iff

added theorem well_founded_of_empty

Modified scripts/nolints.json