Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-27 09:16 ff2aeae9

View on Github →

feat(logic/relation): trans_gen closure (#5129) Mechanical conversion of refl_trans_gen lemmas for just trans_gen.

Estimated changes

Modified src/logic/relation.lean

added theorem relation.trans_gen.trans_gen_closed

added theorem relation.trans_gen.trans_gen_eq_self

added theorem relation.trans_gen.trans_gen_idem

added theorem relation.trans_gen.trans_gen_lift'

added theorem relation.trans_gen.trans_gen_lift

added theorem relation.trans_gen.transitive_trans_gen