Commit 2023-04-03 11:48 59e4a793

View on Github →

feat: port Logic.Hydra (#2290)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Multiset/Basic.lean

Modified Mathlib/Data/Multiset/Sections.lean

Created Mathlib/Logic/Hydra.lean

added theorem Acc.cutExpand

added def Relation.CutExpand

added theorem Relation.acc_of_singleton

added theorem Relation.cutExpand_add_left

added theorem Relation.cutExpand_fibration

added theorem Relation.cutExpand_iff

added theorem Relation.cutExpand_le_invImage_lex

added theorem Relation.cutExpand_singleton

added theorem Relation.cutExpand_singleton_singleton

added theorem Relation.not_cutExpand_zero

added theorem WellFounded.cutExpand