mathlib3

5ca6e9d2 - feat(logic/relation): characterization of the accessible predicate in terms of `well_founded_on` (#16720)

feat(logic/relation): characterization of the accessible predicate in terms of `well_founded_on` (#16720) + Show that `acc r a` (read: `a` is accessible under the relation `r`) if and only if `r` is well-founded on the subset of elements below `a` (transitively) under `r`, including (`refl_trans_gen`) or excluding (`trans_gen`) `a`. Stated as a `list.tfae`. + Move `relation.fibration` (used by the proof) to *logic/relation* to avoid importing *logic/hydra*. Add lemma `acc_trans_gen_iff` used in the proof.