Yury G. Kudryashov

--- [](https://gitpod.io/from-referrer/)

feat(Fin/Parity): add `Fin.even_iff`

1

Motivated by [this](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.28u.20.3A.20Fin.202.29.20.20.E2.86.92.20.28Even.20u.20.E2.86.94.20Even.20u.2Eval.29) Zulip question. --- - [ ] depends on: #8974 [](https://gitpod.io/from-referrer/)

feat(RelClasses): generalize `IsTrans`/`IsRefl` instances

1

--- [](https://gitpod.io/from-referrer/)

feat(AEEqFun): add 3 trivial lemmas

1

--- [](https://gitpod.io/from-referrer/)

feat(order/filter,topology/instances/nnreal): upgrade some lemmas to `iff`

1

* Add `codisjoint.inf_left_sup_inf_right` and `is_compl.le_inf_sup_inf`. * Add `filter.comap_ite`, `filter.comap_max`, and `filter.tendsto_ite`. * Add `real.map_to_nnreal_at_top`, `real.comap_to_nnreal_at_top`, and `real.tendsto_to_nnreal_at_top_iff`. * Rename `tendsto_real_to_nnreal` to `filter.tendsto.real_to_nnreal` so that it can be used with dot...

feat(ENNReal/Real): +1 `@[gcongr]`, +2 lemmas

1

--- [](https://gitpod.io/from-referrer/)

feat(LineDeriv/QuadraticForm): new file

1

Line derivative of a quadratic form is given by its polar bilinear form. --- [](https://gitpod.io/from-referrer/)

feat(LocalExtr/LineDeriv): new file

1

--- [](https://gitpod.io/from-referrer/)

chore(Order/Intervals/Set): move some defs to a new file

5

--- [](https://gitpod.io/from-referrer/)