Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-15 03:13 dd4d8e6a

View on Github →

feat(logic/hydra): basic lemmas on cut_expand (#14408)

Estimated changes

Modified src/logic/hydra.lean

modified def relation.cut_expand

added theorem relation.cut_expand_add_left

modified theorem relation.cut_expand_fibration

modified theorem relation.cut_expand_iff

added theorem relation.cut_expand_singleton

added theorem relation.cut_expand_singleton_singleton

added theorem relation.not_cut_expand_zero