Relation

📁 Source: Mathlib/Logic/Relation.lean

Statistics

Metric	Count
Definitions `EqvGen`, `setoid`, `ReflGen`, `ReflTransGen`, `SymmGen`, `decidableRel`, `instDecidableMapOfExistsAndEq`, `instTransReflTransGen`, `instTransReflTransGenTransGen`, `instTransReflTransGen_1`, `instTransTransGenReflTransGen`, `instTransTransGen_mathlib`, `instTransTransGen_mathlib_1`	13
Theorems `of_downward_closed`, `of_fibration`, `comap`, `eqvGen_eq`, `eqvGen_iff`, `reflexive`, `symmGen`, `symmGen_symm`, `eqvGen_exact`, `eqvGen_sound`, `comap`, `ne_imp_iff`, `rel_of_ne_imp`, `is_equivalence`, `mono`, `instRefl`, `mono`, `to_reflTransGen`, `cases_head`, `cases_head_iff`, `cases_tail`, `cases_tail_iff`, `head`, `head_induction_on`, `lift'`, `mono`, `single`, `swap`, `symmetric`, `total_of_right_unique`, `trans`, `trans_induction_on`, `instRefl`, `instSymm`, `of_ge`, `of_le`, `of_rel`, `of_rel_symm`, `refl`, `rfl`, `swap`, `closed`, `closed'`, `head`, `head'`, `head'_iff`, `head_induction_on`, `lift'`, `mono`, `swap`, `symmetric`, `tail'`, `tail'_iff`, `to_reflTransGen`, `trans_induction_on`, `trans_left`, `trans_right`, `church_rosser`, `comp_assoc`, `comp_eq`, `comp_eq_fun`, `comp_iff`, `eq_comp`, `equivalence_join`, `equivalence_join_reflTransGen`, `eqvGen_iff`, `flip_comp`, `fun_eq_comp`, `iff_comp`, `instIsTransReflTransGen`, `instIsTransTransGen`, `instReflReflTransGen`, `join_of_equivalence`, `join_of_single`, `le_onFun_map`, `map_apply`, `map_apply_apply`, `map_equivalence`, `map_id_id`, `map_map`, `map_mono`, `map_onFun_eq_of_surjective`, `map_onFun_le`, `map_onFun_map_eq_map`, `map_reflexive`, `map_symmetric`, `map_transitive`, `onFun_map_eq_of_injective`, `onFun_map_onFun_eq_onFun`, `onFun_map_onFun_iff_onFun`, `reflGen_eq_self`, `reflGen_iff`, `reflGen_minimal`, `reflGen_transGen`, `reflTransGen_closed`, `reflTransGen_eq_reflGen`, `reflTransGen_eq_self`, `reflTransGen_eq_transGen`, `reflTransGen_idem`, `reflTransGen_iff_eq`, `reflTransGen_iff_eq_or_transGen`, `reflTransGen_minimal`, `reflTransGen_of_equivalence`, `reflTransGen_of_transitive_reflexive`, `reflTransGen_reflGen`, `reflTransGen_swap`, `reflTransGen_transGen`, `reflexive_join`, `reflexive_reflGen`, `reflexive_reflTransGen`, `symmGen_comm`, `symmGen_of_total`, `symmGen_swap`, `symmGen_swap_apply`, `symmetric_join`, `transGen_eq_self`, `transGen_idem`, `transGen_iff`, `transGen_minimal`, `transGen_reflGen`, `transGen_swap`, `transitive_join`, `transitive_reflTransGen`, `transitive_transGen`, `reflexive`, `comap`, `flip_eq`, `iff`, `swap_eq`, `comap`, `flip_eq_iff`, `irrefl_iff_subrelation_ne`, `irreflexive_iff_subrelation_ne`, `reflexive_iff_subrelation_eq`, `reflexive_ne_imp_iff`, `swap_eq_iff`	136
Total	149

Acc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_downward_closed` 📖	—	—	—	—	`of_fibration`
`of_fibration` 📖	—	`Relation.Fibration`	—	—	—

Equivalence

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap` 📖	mathematical	—	`Function.onFun`	—	—
`eqvGen_eq` 📖	mathematical	—	`Relation.EqvGen`	—	`eqvGen_iff`
`eqvGen_iff` 📖	mathematical	—	`Relation.EqvGen`	—	—

IsRefl

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`reflexive` 📖	mathematical	—	`Reflexive`	—	`Std.Refl.reflexive`

LE.le

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`symmGen` 📖	mathematical	—	`Relation.SymmGen`	—	`Relation.SymmGen.of_le`
`symmGen_symm` 📖	mathematical	—	`Relation.SymmGen`	—	`Relation.SymmGen.of_ge`

Quot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eqvGen_exact` 📖	mathematical	—	`Relation.EqvGen`	—	—
`eqvGen_sound` 📖	—	`Relation.EqvGen`	—	—	—

Reflexive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap` 📖	mathematical	`Reflexive`	`Function.onFun`	—	—
`ne_imp_iff` 📖	—	`Reflexive`	—	—	`rel_of_ne_imp`
`rel_of_ne_imp` 📖	—	`Reflexive`	—	—	—

Relation

Definitions

Name	Category	Theorems
`EqvGen` 📖	CompData	18 math math: `TopCat.GlueData.eqvGen_of_π_eq`, `CategoryTheory.Functor.eqvGen_colimitTypeRel_iff_of_isFiltered`, `CategoryTheory.Quotient.functor_homRel_eq_compClosure_eqvGen`, `CategoryTheory.Limits.Types.colimit_eq`, `CategoryTheory.Quotient.compClosure.congruence`, `EqvGen.is_equivalence`, `Quot.subsingleton_iff`, `eqvGen_iff`, `CategoryTheory.Limits.Types.FilteredColimit.eqvGen_colimitTypeRel_of_rel`, `CategoryTheory.Limits.Types.FilteredColimit.rel_eq_eqvGen_colimitTypeRel`, `FreeGroup.eqvGen_step_iff_join_red`, `FreeAddGroup.eqvGen_step_iff_join_red`, `Quot.eqvGen_exact`, `Equivalence.eqvGen_iff`, `CategoryTheory.Functor.ιColimitType_eq_iff`, `Quot.eq`, `RingQuot.eqvGen_rel_eq`, `Equivalence.eqvGen_eq`
`ReflGen` 📖	CompData	9 math math: `transGen_reflGen`, `reflGen_eq_self`, `reflTransGen_reflGen`, `reflGen_transGen`, `ReflGen.instRefl`, `wcovBy_eq_reflGen_covBy`, `reflexive_reflGen`, `reflGen_iff`, `reflTransGen_eq_reflGen`
`ReflTransGen` 📖	CompData	40 math math: `ReflTransGen.cases_tail_iff`, `reflTransGen_of_succ_of_ge`, `reflTransGen_swap`, `ReflTransGen.cases_head_iff`, `List.relationReflTransGen_of_exists_isChain`, `reflTransGen_of_pred`, `TransGen.tail'_iff`, `reflexive_reflTransGen`, `ReflGen.to_reflTransGen`, `reflTransGen_eq_transGen`, `SimpleGraph.reachable_fromEdgeSet_eq_reflTransGen_toRel`, `reflTransGen_of_pred_of_ge`, `Set.WellFoundedOn.acc_iff_wellFoundedOn`, `transGen_reflGen`, `ReflTransGen.symmetric`, `reflTransGen_eq_self`, `le_iff_reflTransGen_covBy`, `reflTransGen_of_succ_of_le`, `reflTransGen_reflGen`, `reflGen_transGen`, `reflTransGen_idem`, `reflTransGen_iff_eq_or_transGen`, `transitive_reflTransGen`, `SimpleGraph.reachable_iff_reflTransGen`, `ReflTransGen.single`, `reflTransGen_transGen`, `TransGen.head'_iff`, `reflTransGen_of_pred_of_le`, `TransGen.to_reflTransGen`, `List.relationReflTransGen_of_exists_isChain_cons`, `reflTransGen_iff_eq`, `List.relationReflTransGen_of_exists_chain_cons`, `transGen_wcovBy_eq_reflTransGen_covBy`, `SimpleGraph.reachable_fromEdgeSet_fromRel_eq_reflTransGen`, `SimpleGraph.reachable_eq_reflTransGen`, `reflTransGen_wcovBy_eq_reflTransGen_covBy`, `instReflReflTransGen`, `reflTransGen_of_succ`, `instIsTransReflTransGen`, `reflTransGen_eq_reflGen`
`SymmGen` 📖	MathDef	25 math math: `AntisymmRel.symmGen_congr`, `symmGen_of_total`, `SymmGen.of_lt`, `SymmGen.of_gt`, `SymmGen.rfl`, `SymmGen.refl`, `AntisymmRel.symmGen`, `LT.lt.symmGen`, `SymmGen.of_le`, `SymmGen.instRefl`, `IsTotal.compRel`, `AntisymmRel.symmGen_congr_left`, `symmGen_swap`, `SymmGen.of_ge`, `symmGen_swap_apply`, `SymmGen.of_rel_symm`, `AntisymmRel.symmGen_congr_right`, `symmGen_comm`, `not_symmGen_iff`, `SymmGen.of_rel`, `LE.le.symmGen_symm`, `LT.lt.symmGen_symm`, `SymmGen.instSymm`, `not_incompRel_iff_symmGen`, `LE.le.symmGen`
`instDecidableMapOfExistsAndEq` 📖	CompOp	4 math math: `SimpleGraph.card_edgeFinset_map`, `SimpleGraph.edgeFinset_map`, `SimpleGraph.cliqueFinset_map_of_equiv`, `SimpleGraph.cliqueFinset_map`
`instTransReflTransGen` 📖	CompOp	—
`instTransReflTransGenTransGen` 📖	CompOp	—
`instTransReflTransGen_1` 📖	CompOp	—
`instTransTransGenReflTransGen` 📖	CompOp	—
`instTransTransGen_mathlib` 📖	CompOp	—
`instTransTransGen_mathlib_1` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`church_rosser` 📖	mathematical	`ReflGen` `ReflTransGen`	`Join`	—	`ReflTransGen.trans`
`comp_assoc` 📖	mathematical	—	`Comp`	—	—
`comp_eq` 📖	mathematical	—	`Comp`	—	`comp_eq_fun`
`comp_eq_fun` 📖	mathematical	—	`Comp`	—	—
`comp_iff` 📖	mathematical	—	`Comp`	—	—
`eq_comp` 📖	mathematical	—	`Comp`	—	`fun_eq_comp`
`equivalence_join` 📖	—	`Reflexive` `Transitive` `Join`	—	—	`reflexive_join` `symmetric_join` `transitive_join`
`equivalence_join_reflTransGen` 📖	mathematical	`ReflGen` `ReflTransGen`	`Join`	—	`equivalence_join` `reflexive_reflTransGen` `transitive_reflTransGen` `church_rosser`
`eqvGen_iff` 📖	mathematical	—	`EqvGen`	—	—
`flip_comp` 📖	mathematical	—	`Comp`	—	—
`fun_eq_comp` 📖	mathematical	—	`Comp`	—	—
`iff_comp` 📖	mathematical	—	`Comp`	—	—
`instIsTransReflTransGen` 📖	mathematical	—	`IsTrans` `ReflTransGen`	—	`ReflTransGen.trans`
`instIsTransTransGen` 📖	mathematical	—	`IsTrans`	—	—
`instReflReflTransGen` 📖	mathematical	—	`ReflTransGen`	—	—
`join_of_equivalence` 📖	—	`Join`	—	—	—
`join_of_single` 📖	mathematical	`Reflexive`	`Join`	—	—
`le_onFun_map` 📖	mathematical	—	`Function.onFun` `Map`	—	—
`map_apply` 📖	mathematical	—	`Map`	—	—
`map_apply_apply` 📖	mathematical	—	`Map`	—	—
`map_equivalence` 📖	mathematical	—	`Map`	—	`map_reflexive` `Equivalence.reflexive` `map_symmetric` `Equivalence.symmetric` `map_transitive` `Equivalence.transitive`
`map_id_id` 📖	mathematical	—	`Map`	—	—
`map_map` 📖	mathematical	—	`Map`	—	—
`map_mono` 📖	—	`Map`	—	—	—
`map_onFun_eq_of_surjective` 📖	mathematical	—	`Map` `Function.onFun`	—	—
`map_onFun_le` 📖	mathematical	—	`Map` `Function.onFun`	—	—
`map_onFun_map_eq_map` 📖	mathematical	—	`Map` `Function.onFun`	—	—
`map_reflexive` 📖	mathematical	`Reflexive`	`Map`	—	—
`map_symmetric` 📖	mathematical	`Symmetric`	`Map`	—	—
`map_transitive` 📖	mathematical	`Transitive`	`Map`	—	—
`onFun_map_eq_of_injective` 📖	mathematical	—	`Function.onFun` `Map`	—	—
`onFun_map_onFun_eq_onFun` 📖	mathematical	—	`Function.onFun` `Map`	—	—
`onFun_map_onFun_iff_onFun` 📖	mathematical	—	`Map` `Function.onFun`	—	—
`reflGen_eq_self` 📖	mathematical	`Reflexive`	`ReflGen`	—	—
`reflGen_iff` 📖	mathematical	—	`ReflGen`	—	—
`reflGen_minimal` 📖	—	`Reflexive` `ReflGen`	—	—	`reflGen_eq_self` `ReflGen.mono`
`reflGen_transGen` 📖	mathematical	—	`ReflGen` `ReflTransGen`	—	—
`reflTransGen_closed` 📖	—	`ReflTransGen`	—	—	`ReflTransGen.lift'`
`reflTransGen_eq_reflGen` 📖	mathematical	`Transitive`	`ReflTransGen` `ReflGen`	—	`reflGen_transGen` `transGen_eq_self`
`reflTransGen_eq_self` 📖	mathematical	`Reflexive` `Transitive`	`ReflTransGen`	—	`ReflTransGen.single`
`reflTransGen_eq_transGen` 📖	mathematical	`Reflexive`	`ReflTransGen`	—	`transGen_reflGen` `reflGen_eq_self`
`reflTransGen_idem` 📖	mathematical	—	`ReflTransGen`	—	`reflTransGen_eq_self` `reflexive_reflTransGen` `transitive_reflTransGen`
`reflTransGen_iff_eq` 📖	mathematical	—	`ReflTransGen`	—	`ReflTransGen.cases_head_iff`
`reflTransGen_iff_eq_or_transGen` 📖	mathematical	—	`ReflTransGen`	—	`TransGen.tail'` `TransGen.to_reflTransGen`
`reflTransGen_minimal` 📖	—	`Reflexive` `Transitive` `ReflTransGen`	—	—	`reflTransGen_of_transitive_reflexive`
`reflTransGen_of_equivalence` 📖	—	`ReflTransGen`	—	—	`reflTransGen_of_transitive_reflexive`
`reflTransGen_of_transitive_reflexive` 📖	—	`Reflexive` `Transitive` `ReflTransGen`	—	—	`reflTransGen_eq_self` `ReflTransGen.mono`
`reflTransGen_reflGen` 📖	mathematical	—	`ReflTransGen` `ReflGen`	—	`reflGen_eq_self` `reflexive_reflGen`
`reflTransGen_swap` 📖	mathematical	—	`ReflTransGen` `Function.swap`	—	`ReflTransGen.swap`
`reflTransGen_transGen` 📖	mathematical	—	`ReflTransGen`	—	`transGen_idem`
`reflexive_join` 📖	mathematical	`Reflexive`	`Join`	—	—
`reflexive_reflGen` 📖	mathematical	—	`Reflexive` `ReflGen`	—	—
`reflexive_reflTransGen` 📖	mathematical	—	`Reflexive` `ReflTransGen`	—	—
`symmGen_comm` 📖	mathematical	—	`SymmGen`	—	—
`symmGen_of_total` 📖	mathematical	—	`SymmGen`	—	—
`symmGen_swap` 📖	mathematical	—	`SymmGen` `Function.swap`	—	—
`symmGen_swap_apply` 📖	mathematical	—	`SymmGen` `Function.swap`	—	—
`symmetric_join` 📖	mathematical	—	`Symmetric` `Join`	—	—
`transGen_eq_self` 📖	—	`Transitive`	—	—	—
`transGen_idem` 📖	—	—	—	—	`transGen_eq_self` `transitive_transGen`
`transGen_iff` 📖	—	—	—	—	—
`transGen_minimal` 📖	—	`Transitive`	—	—	`transGen_eq_self` `TransGen.mono`
`transGen_reflGen` 📖	mathematical	—	`ReflGen` `ReflTransGen`	—	`reflTransGen_idem` `TransGen.to_reflTransGen` `TransGen.mono` `ReflGen.to_reflTransGen` `reflTransGen_iff_eq_or_transGen`
`transGen_swap` 📖	mathematical	—	`Function.swap`	—	`TransGen.swap`
`transitive_join` 📖	—	`Transitive` `Join`	—	—	—
`transitive_reflTransGen` 📖	mathematical	—	`Transitive` `ReflTransGen`	—	`ReflTransGen.trans`
`transitive_transGen` 📖	mathematical	—	`Transitive`	—	—

Relation.EqvGen

Definitions

Name	Category	Theorems
`setoid` 📖	CompOp	9 math math: `Setoid.eqvGen_le`, `Setoid.sSup_def`, `Setoid.sup_eq_eqvGen`, `Setoid.sup_def`, `Setoid.eqvGen_mono`, `Setoid.sSup_eq_eqvGen`, `Setoid.eqvGen_eq`, `Setoid.eqvGen_idem`, `Setoid.eqvGen_of_setoid`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`is_equivalence` 📖	mathematical	—	`Relation.EqvGen`	—	—
`mono` 📖	—	`Relation.EqvGen`	—	—	—

Relation.ReflGen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instRefl` 📖	mathematical	—	`Relation.ReflGen`	—	—
`mono` 📖	—	`Relation.ReflGen`	—	—	—
`to_reflTransGen` 📖	mathematical	`Relation.ReflGen`	`Relation.ReflTransGen`	—	—

Relation.ReflTransGen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cases_head` 📖	—	`Relation.ReflTransGen`	—	—	`head_induction_on`
`cases_head_iff` 📖	mathematical	—	`Relation.ReflTransGen`	—	`cases_head` `head`
`cases_tail` 📖	—	`Relation.ReflTransGen`	—	—	`cases_tail_iff`
`cases_tail_iff` 📖	mathematical	—	`Relation.ReflTransGen`	—	—
`head` 📖	—	`Relation.ReflTransGen`	—	—	—
`head_induction_on` 📖	—	`Relation.ReflTransGen` `refl` `head`	—	—	`head`
`lift'` 📖	—	`Relation.ReflTransGen`	—	—	`Relation.reflTransGen_idem` `lift`
`mono` 📖	—	`Relation.ReflTransGen`	—	—	`lift`
`single` 📖	mathematical	—	`Relation.ReflTransGen`	—	—
`swap` 📖	mathematical	`Relation.ReflTransGen`	`Function.swap`	—	`head`
`symmetric` 📖	mathematical	`Symmetric`	`Relation.ReflTransGen`	—	`head`
`total_of_right_unique` 📖	—	`Relator.RightUnique` `Relation.ReflTransGen`	—	—	`cases_head` `single`
`trans` 📖	—	`Relation.ReflTransGen`	—	—	—
`trans_induction_on` 📖	—	`Relation.ReflTransGen` `refl` `single` `trans`	—	—	`single` `trans`

Relation.SymmGen

Definitions

Name	Category	Theorems
`decidableRel` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instRefl` 📖	mathematical	—	`Relation.SymmGen`	—	`refl`
`instSymm` 📖	mathematical	—	`Relation.SymmGen`	—	`symm`
`of_ge` 📖	mathematical	—	`Relation.SymmGen`	—	`of_rel_symm`
`of_le` 📖	mathematical	—	`Relation.SymmGen`	—	`of_rel`
`of_rel` 📖	mathematical	—	`Relation.SymmGen`	—	—
`of_rel_symm` 📖	mathematical	—	`Relation.SymmGen`	—	—
`refl` 📖	mathematical	—	`Relation.SymmGen`	—	`of_rel` `refl`
`rfl` 📖	mathematical	—	`Relation.SymmGen`	—	`refl`
`swap` 📖	mathematical	`Relation.SymmGen`	`Function.swap`	—	`of_rel` `of_rel_symm`

Relation.TransGen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closed` 📖	—	—	—	—	`lift'`
`closed'` 📖	—	—	—	—	`head_induction_on`
`head` 📖	—	—	—	—	`head'` `to_reflTransGen`
`head'` 📖	—	`Relation.ReflTransGen`	—	—	`trans_left`
`head'_iff` 📖	mathematical	—	`Relation.ReflTransGen`	—	`head'`
`head_induction_on` 📖	—	`head`	—	—	`head`
`lift'` 📖	—	—	—	—	`Relation.transGen_idem` `lift`
`mono` 📖	—	—	—	—	`lift`
`swap` 📖	mathematical	—	`Function.swap`	—	`head`
`symmetric` 📖	—	`Symmetric`	—	—	`head`
`tail'` 📖	—	`Relation.ReflTransGen`	—	—	—
`tail'_iff` 📖	mathematical	—	`Relation.ReflTransGen`	—	`to_reflTransGen` `tail'`
`to_reflTransGen` 📖	mathematical	—	`Relation.ReflTransGen`	—	`Relation.ReflTransGen.single`
`trans_induction_on` 📖	—	—	—	—	—
`trans_left` 📖	—	`Relation.ReflTransGen`	—	—	—
`trans_right` 📖	—	`Relation.ReflTransGen`	—	—	`tail'`

Std.Refl

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`reflexive` 📖	mathematical	—	`Reflexive`	—	—

Symmetric

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap` 📖	mathematical	`Symmetric`	`Function.onFun`	—	—
`flip_eq` 📖	—	`Symmetric`	—	—	`iff`
`iff` 📖	—	`Symmetric`	—	—	—
`swap_eq` 📖	mathematical	`Symmetric`	`Function.swap`	—	`flip_eq`

Transitive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap` 📖	mathematical	`Transitive`	`Function.onFun`	—	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`flip_eq_iff` 📖	mathematical	—	`Symmetric`	—	`Symmetric.flip_eq`
`irrefl_iff_subrelation_ne` 📖	—	—	—	—	—
`irreflexive_iff_subrelation_ne` 📖	—	—	—	—	`irrefl_iff_subrelation_ne`
`reflexive_iff_subrelation_eq` 📖	mathematical	—	`Reflexive`	—	—
`reflexive_ne_imp_iff` 📖	—	—	—	—	`Reflexive.ne_imp_iff` `Std.Refl.reflexive`
`swap_eq_iff` 📖	mathematical	—	`Function.swap` `Symmetric`	—	`flip_eq_iff`

---

← Back to Index