Rel

Statistics

Metric	Count
Definitions `Rel`, `Rel`, `Rel`, `Rel`, `Rel`, `Rel`, `Rel`, `Rel`, `Rel`, `Rel`, `Rel`, `graph`, `tupleGraph`, `Rel`, `Rel`, `Rel`, `Rel`, `Rel`, `SetRel`, `IsIrrefl`, `IsRefl`, `IsSymm`, `IsTrans`, `IsWellFounded`, `cod`, `comp`, `core`, `dom`, `id`, `image`, `inv`, `preimage`, `restrictDomain`, `symmetrize`, `«term_~[_]_»`, `«term_○_»`, `Rel`, `Rel`, `Rel`, `Rel`, `Rel`, `Rel`, `Rel`	43
Theorems `graph_inv`, `graph_comp`, `graph_id`, `graph_inj`, `graph_injective`, `mem_graph`, `relComp`, `image_eq`, `preimage_eq`, `preimage_eq_core`, `comp`, `sInter`, `sInter`, `sInter`, `cod_empty`, `cod_eq_empty_iff`, `cod_inv`, `cod_mono`, `cod_univ`, `comm`, `comp_assoc`, `comp_empty`, `comp_eq_self`, `comp_iUnion`, `comp_id`, `comp_sUnion`, `comp_subset_comp`, `comp_subset_comp_left`, `comp_subset_comp_right`, `comp_subset_self`, `comp_univ`, `core_comp`, `core_id`, `core_inter`, `core_mono`, `core_subset_core`, `core_union_subset`, `core_univ`, `dom_empty`, `dom_eq_empty_iff`, `dom_inv`, `dom_mono`, `dom_univ`, `empty_comp`, `exists_eq_singleton_of_prod_subset_id`, `exists_graph_eq_iff`, `iUnion_comp`, `id_comp`, `id_subset`, `id_subset_iff`, `image_comp`, `image_core_gc`, `image_empty_left`, `image_empty_right`, `image_eq_biUnion`, `image_eq_cod_of_dom_subset`, `image_iUnion`, `image_id`, `image_inter_dom`, `image_inter_subset`, `image_inv`, `image_mono`, `image_sUnion`, `image_subset_iff`, `image_subset_image`, `image_subset_image_left`, `image_union`, `image_univ_left`, `image_univ_right`, `instIsIrreflSetOfProdMatch_1PropOfIrrefl`, `instIsSymmInv`, `instIsTransSetOfProdMatch_1PropOfIsTrans`, `inter_cod_subset_image_preimage`, `inter_dom_subset_preimage_image`, `inv_comp`, `inv_empty`, `inv_eq_self`, `inv_eq_self_iff`, `inv_id`, `inv_inv`, `inv_mono`, `inv_univ`, `irrefl`, `isRefl_iInter`, `isRefl_inter`, `isRefl_mono`, `isRefl_preimage`, `isRefl_univ`, `isSymm_comp_inv`, `isSymm_comp_self`, `isSymm_empty`, `isSymm_iInter`, `isSymm_id`, `isSymm_image`, `isSymm_inter`, `isSymm_inv_comp`, `isSymm_preimage`, `isSymm_symmetrize`, `isSymm_univ`, `isTrans_empty`, `isTrans_iInter`, `isTrans_id`, `isTrans_iff_comp_subset_self`, `isTrans_inter`, `isTrans_preimage`, `isTrans_singleton`, `isTrans_symmetrize`, `isTrans_univ`, `left_subset_comp`, `mem_cod`, `mem_comp`, `mem_core`, `mem_dom`, `mem_id`, `mem_image`, `mem_inv`, `mem_preimage`, `preimage_comp`, `preimage_empty_left`, `preimage_empty_right`, `preimage_eq_biUnion`, `preimage_eq_dom_of_cod_subset`, `preimage_eq_image`, `preimage_iUnion`, `preimage_id`, `preimage_inter_cod`, `preimage_inter_subset`, `preimage_inv`, `preimage_mono`, `preimage_sUnion`, `preimage_subset_preimage`, `preimage_subset_preimage_left`, `preimage_union`, `preimage_univ_left`, `preimage_univ_right`, `prodMk_mem_comp`, `prod_comp_prod`, `prod_comp_prod_of_disjoint`, `prod_comp_prod_of_inter_nonempty`, `prod_subset_comm`, `refl`, `rfl`, `right_subset_comp`, `sUnion_comp`, `self_subset_image`, `self_subset_preimage`, `subset_iterate_comp`, `subset_symmetrize`, `symmetrize_mono`, `symmetrize_subset_inv`, `symmetrize_subset_self`, `trans`, `univ_comp`	153
Total	196

AddConGen

Definitions

Name	Category	Theorems
`Rel` 📖	CompData	—

AlgebraicGeometry.Scheme.GlueData

Definitions

Name	Category	Theorems
`Rel` 📖	MathDef	1 math math: `ι_eq_iff`

CategoryTheory.FreeBicategory

Definitions

Name	Category	Theorems
`Rel` 📖	CompData	8 math math: `mk_left_unitor_inv`, `mk_right_unitor_inv`, `mk_id`, `mk_left_unitor_hom`, `mk_associator_hom`, `mk_associator_inv`, `lift_toPrelaxFunctor_toPrelaxFunctorStruct_map₂`, `mk_right_unitor_hom`

CategoryTheory.Limits.Types.FilteredColimit

Definitions

Name	Category	Theorems
`Rel` 📖	MathDef	4 math math: `colimit_eq_iff_aux`, `rel_eq_eqvGen_colimitTypeRel`, `rel_equiv`, `rel_of_colimitTypeRel`

CategoryTheory.Limits.Types.Pushout

Definitions

Name	Category	Theorems
`Rel` 📖	CompData	1 math math: `quot_mk_eq_iff`

CliffordAlgebra

Definitions

Name	Category	Theorems
`Rel` 📖	CompData	21 math math: `involute_prod_map_ι`, `contractRight_mul_ι`, `changeFormAux_changeFormAux`, `EquivEven.ι_eq_v_add_smul_e0`, `foldr'Aux_foldr'Aux`, `spinGroup.conjAct_smul_range_ι`, `submodule_comap_mul_reverse`, `submodule_map_pow_reverse`, `contractLeft_ι_mul`, `star_smul`, `CliffordAlgebraQuaternion.ofQuaternion_mk`, `pinGroup.conjAct_smul_range_ι`, `submodule_map_mul_reverse`, `evenOdd_mul_le`, `iSup_ι_range_eq_top`, `submodule_comap_pow_reverse`, `ExteriorAlgebra.ιMulti_succ_curryLeft`, `ExteriorAlgebra.invertibleAlgebraMapEquiv_symm_apply_invOf_toQuot`, `exteriorPower.zeroEquiv_symm_apply`, `contractLeftAux_contractLeftAux`, `lipschitzGroup.conjAct_smul_range_ι`

ComplexShape

Definitions

Name	Category	Theorems
`Rel` 📖	MathDef	21 math math: `exists_distinct_next_or`, `exists_distinct_prev_or`, `down_Rel`, `up_Rel`, `symm_Rel`, `not_rel_self`, `down'_Rel`, `AlgebraicTopology.DoldKan.cs_down_0_not_rel_left`, `down'_mk`, `down_mk`, `AlgebraicTopology.DoldKan.c_mk`, `HomologicalComplex.alternatingConst_d`, `not_rel_of_eq`, `subsingleton_prev`, `HasNoLoop.not_rel_self`, `ext_iff`, `subsingleton_next`, `refl_Rel`, `Embedding.rel_iff`, `Homotopy.nullHomotopy'_hom`, `up'_Rel`

ConGen

Definitions

Name	Category	Theorems
`Rel` 📖	CompData	—

Equiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`graph_inv` 📖	mathematical	—	`Function.graph` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm` `SetRel.inv`	—	`Set.ext` `apply_symm_apply` `symm_apply_apply`

FreeAlgebra

Definitions

Name	Category	Theorems
`Rel` 📖	CompData	2 math math: `ι_def`, `quot_mk_eq_ι`

FreeLieAlgebra

Definitions

Name	Category	Theorems
`Rel` 📖	CompData	—

Function

Definitions

Name	Category	Theorems
`graph` 📖	CompOp	14 math math: `Set.image_eq`, `graph_inj`, `Filter.tendsto_iff_rtendsto`, `Set.preimage_eq`, `CategoryTheory.RelCat.rel_graphFunctor_map`, `graph_injective`, `Equiv.graph_inv`, `Set.preimage_eq_core`, `Set.TermDefinable₁.definable₂_graph`, `graph_id`, `mem_graph`, `Filter.tendsto_iff_rtendsto'`, `SetRel.exists_graph_eq_iff`, `graph_comp`
`tupleGraph` 📖	CompOp	1 math math: `Set.TermDefinable.definable_tupleGraph`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`graph_comp` 📖	mathematical	—	`graph` `SetRel.comp`	—	`Set.ext`
`graph_id` 📖	mathematical	—	`graph` `SetRel.id`	—	—
`graph_inj` 📖	mathematical	—	`graph`	—	`graph_injective`
`graph_injective` 📖	mathematical	—	`SetRel` `graph`	—	—
`mem_graph` 📖	mathematical	—	`SetRel` `Set.instMembership` `graph`	—	—

Function.Coequalizer

Definitions

Name	Category	Theorems
`Rel` 📖	CompData	1 math math: `TopCat.GlueData.eqvGen_of_π_eq`

Monoid.CoprodI

Definitions

Name	Category	Theorems
`Rel` 📖	CompData	1 math math: `of_apply`

Monotone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`relComp` 📖	mathematical	`Monotone` `SetRel` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `Set.instBooleanAlgebra`	`SetRel.comp`	—	—

Multiset

Definitions

Name	Category	Theorems
`Rel` 📖	CompData	25 math math: `rel_of_forall`, `rel_flip`, `rel_map_left`, `rel_refl_of_refl_on`, `UniqueFactorizationMonoid.factors_pow`, `UniqueFactorizationMonoid.factors_rel_of_associated`, `UniqueFactorizationMonoid.factors_unique`, `rel_cons_left`, `rel_map_right`, `mem_sections`, `rel_add_left`, `rel_replicate_left`, `Associates.rel_associated_iff_map_eq_map`, `prime_factors_unique`, `rel_add_right`, `rel_flip_eq`, `rel_eq`, `rel_iff`, `rel_eq_refl`, `rel_cons_right`, `rel_replicate_right`, `rel_zero_right`, `UniqueFactorizationMonoid.factors_mul`, `rel_zero_left`, `rel_map`

RingConGen

Definitions

Name	Category	Theorems
`Rel` 📖	CompData	1 math math: `RingQuot.eqvGen_rel_eq`

RingQuot

Definitions

Name	Category	Theorems
`Rel` 📖	CompData	14 math math: `add_quot`, `preLift_def`, `LinearAlgebra.FreeProduct.ι_apply`, `mkRingHom_def`, `mul_quot`, `pow_quot`, `zero_quot`, `sub_quot`, `smul_quot`, `preLiftAlgHom_def`, `ExteriorAlgebra.invertibleAlgebraMapEquiv_symm_apply_invOf_toQuot`, `one_quot`, `neg_quot`, `eqvGen_rel_eq`

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`image_eq` 📖	mathematical	—	`image` `SetRel.image` `Function.graph`	—	—
`preimage_eq` 📖	mathematical	—	`preimage` `SetRel.preimage` `Function.graph`	—	—
`preimage_eq_core` 📖	mathematical	—	`preimage` `SetRel.core` `Function.graph`	—	—

SetRel

Definitions

Name	Category	Theorems
`IsIrrefl` 📖	MathDef	1 math math: `instIsIrreflSetOfProdMatch_1PropOfIrrefl`
`IsRefl` 📖	MathDef	9 math math: `IsRefl.comp`, `isRefl_of_mem_uniformity`, `isRefl_preimage`, `isRefl_univ`, `isRefl_inter`, `id_subset_iff`, `Dynamics.isRefl_dynEntourage`, `isRefl_hausdorffEntourage`, `isRefl_mono`
`IsSymm` 📖	MathDef	34 math math: `IsUltraUniformity.mem_nhds_iff_symm_trans`, `Dynamics.isSymm_dynEntourage`, `IsSymmetricRel.cauchyFilter_gen`, `comp_open_symm_mem_uniformity_sets`, `PseudoMetric.isSymm_closedBall`, `isSymm_id`, `closure_eq_uniformity`, `isSymm_inv_comp`, `PseudoMetric.isSymm_ball`, `CauchyFilter.isSymm_gen`, `isSymm_comp_inv`, `comp_symm_mem_uniformity_sets`, `UniformSpace.mem_nhds_iff_symm`, `isSymm_comp_self`, `UniformSpace.hasBasis_nhds`, `isSymm_symmetrize`, `uniformity_hasBasis_open_symmetric`, `isSymm_univ`, `isSymm_inter`, `isSymm_hausdorffEntourage`, `IsSymm_entourageProd`, `comp_comp_symm_mem_uniformity_sets`, `isSymm_preimage`, `PseudoMetric.isSymmetricRel_closedBall`, `PseudoMetric.isSymmetricRel_ball`, `isSymm_empty`, `UniformSpace.has_seq_basis`, `symm_of_uniformity`, `inv_eq_self_iff`, `IsUltraUniformity.hasBasis`, `instIsSymmInv`, `UniformSpace.hasBasis_symmetric`, `UniformSpace.hasBasis_nhds_prod`, `isSymm_image`
`IsTrans` 📖	MathDef	20 math math: `isTrans_preimage`, `CauchyFilter.isTrans_gen`, `IsUltraUniformity.mem_nhds_iff_symm_trans`, `isTrans_hausdorffEntourage`, `PseudoMetric.IsUltra.isTransitiveRel_closedBall`, `PseudoMetric.IsUltra.isTrans_closedBall`, `isTrans_entourageProd`, `PseudoMetric.IsUltra.isTransitiveRel_ball`, `isTrans_id`, `instIsTransSetOfProdMatch_1PropOfIsTrans`, `IsTransitiveRel.cauchyFilter_gen`, `PseudoMetric.IsUltra.isTrans_ball`, `IsTransitiveRel.entourageProd`, `isTrans_inter`, `isTrans_symmetrize`, `isTrans_empty`, `IsUltraUniformity.hasBasis`, `isTrans_singleton`, `isTrans_univ`, `isTrans_iff_comp_subset_self`
`IsWellFounded` 📖	MathDef	2 math math: `IsWellFounded.inv_of_finiteDimensional`, `IsWellFounded.of_finiteDimensional`
`cod` 📖	CompOp	11 math math: `cod_inv`, `cod_mono`, `preimage_inter_cod`, `mem_cod`, `inter_cod_subset_image_preimage`, `image_univ_right`, `dom_inv`, `cod_univ`, `cod_eq_empty_iff`, `cod_empty`, `univ_comp`
`comp` 📖	CompOp	99 math math: `Dynamics.coverEntropyInfEntourage_le_netEntropyInfEntourage`, `Dynamics.coverEntropyEntourage_le_coverEntropyInfEntourage`, `comp_subset_comp`, `comp3_mem_uniformity`, `comp_iUnion`, `comp_le_uniformity3`, `mem_comp`, `comp_subset_comp_right`, `compRel_mono`, `Filter.rcomap_compose`, `comp_symm_of_uniformity`, `UniformSpace.mem_ball_comp`, `prod_comp_prod_of_inter_nonempty`, `UniformSpace.Core.comp_mem_uniformity_sets`, `UniformSpace.comp`, `prodMk_mem_compRel`, `IsRefl.comp`, `Dynamics.IsDynCoverOf.iterate_le_pow`, `uniformity_lift_le_comp`, `prod_comp_prod`, `inv_comp`, `Filter.rcomap'_compose`, `sUnion_comp`, `compRel_right_mono`, `UniformSpace.mem_comp_of_mem_ball`, `comp_subset_comp_left`, `Dynamics.IsDynCoverOf.preimage`, `compRel_left_mono`, `Dynamics.coverMincard_closure_le`, `Filter.rcomap'_rcomap'`, `Dynamics.coverEntropyEntourage_le_netEntropyEntourage`, `comp_open_symm_mem_uniformity_sets`, `id_comp`, `left_subset_comp`, `right_subset_compRel`, `closure_eq_uniformity`, `prod_comp_prod_of_disjoint`, `right_subset_comp`, `isSymm_inv_comp`, `comp_empty`, `comp_eq_self`, `comp_sUnion`, `Monotone.relComp`, `Dynamics.le_coverEntropyEntourage_image`, `lift'_comp_uniformity`, `subset_comp_self`, `core_comp`, `isSymm_comp_inv`, `comp_symm_mem_uniformity_sets`, `isTransitiveRel_iff_comp_subset_self`, `hausdorffEntourage_comp`, `isSymm_comp_self`, `compRel_assoc`, `preimage_comp`, `subset_iterate_compRel`, `Dynamics.IsDynCoverOf.coverEntropyEntourage_le_log_card_div`, `subset_comp_self_of_mem_uniformity`, `Dynamics.dynEntourage_comp_subset`, `comp_mem_uniformity_sets`, `Dynamics.IsDynCoverOf.closure`, `Dynamics.coverEntropyEntourage_le_log_coverMincard_div`, `Dynamics.coverMincard_le_pow`, `Dynamics.coverMincard_mul_le_pow`, `id_compRel`, `comp_subset_self`, `left_subset_compRel`, `eventually_uniformity_iterate_comp_subset`, `comp_le_uniformity`, `UniformSpace.mem_comp_comp`, `IsTransitiveRel.comp_eq_of_idRel_subset`, `Dynamics.coverMincard_le_netMaxcard`, `Dynamics.coverEntropyInfEntourage_closure`, `Filter.rmap_compose`, `Dynamics.coverEntropyEntourage_closure`, `Filter.rcomap_rcomap`, `comp_comp_symm_mem_uniformity_sets`, `mem_compRel`, `closure_eq_inter_uniformity`, `IsOpen.relComp`, `Monotone.compRel`, `Dynamics.mem_ball_dynEntourage_comp`, `prodMk_mem_comp`, `Dynamics.le_coverEntropyInfEntourage_image`, `empty_comp`, `CategoryTheory.RelCat.Hom.rel_comp`, `image_comp`, `iUnion_comp`, `comp_assoc`, `Dynamics.le_coverMincard_image`, `comp_univ`, `IsTransitiveRel.comp_subset_self`, `Filter.rmap_rmap`, `Function.graph_comp`, `UniformSpace.Core.comp`, `eventually_uniformity_comp_subset`, `subset_iterate_comp`, `comp_id`, `isTrans_iff_comp_subset_self`, `univ_comp`
`core` 📖	CompOp	16 math math: `image_subset_iff`, `core_union_subset`, `Filter.rtendsto_def`, `core_mono`, `core_id`, `Filter.rcomap_sets`, `image_core_gc`, `core_subset_core`, `mem_core`, `core_inter`, `core_comp`, `Set.preimage_eq_core`, `Filter.mem_rmap`, `core_univ`, `Filter.rmap_sets`, `rtendsto_nhds`
`dom` 📖	CompOp	13 math math: `preimage_univ_right`, `preimage_eq_dom_of_cod_subset`, `cod_inv`, `image_eq_cod_of_dom_subset`, `dom_mono`, `inter_dom_subset_preimage_image`, `dom_eq_empty_iff`, `dom_univ`, `dom_inv`, `image_inter_dom`, `dom_empty`, `mem_dom`, `comp_univ`
`id` 📖	CompOp	32 math math: `discreteUniformity_iff_eq_principal_relId`, `bot_uniformity`, `core_id`, `isCover_relId`, `id_comp`, `isSymm_id`, `discreteUniformity_iff_setRelId_mem_uniformity`, `discreteUniformity_iff_relId_mem_uniformity`, `discreteUniformity_iff_eq_principal_setRelId`, `isCover_id`, `DiscreteUniformity.relId_mem_uniformity`, `isTrans_id`, `DiscreteUniformity.eq_principal_setRelId`, `UniformSpace.uniformSpace_eq_bot`, `DiscreteUniformity.eq_principal_relId`, `discreteUniformity_iff_idRel_mem_uniformity`, `mem_id`, `Function.graph_id`, `discreteUniformity_iff_eq_principal_idRel`, `id_subset_iff`, `id_subset`, `hausdorffEntourage_id`, `DiscreteUniformity.idRel_mem_uniformity`, `image_id`, `refl_le_uniformity`, `inv_id`, `DiscreteUniformity.eq_principal_idRel`, `preimage_id`, `comap_uniformity_of_spaced_out`, `CategoryTheory.RelCat.Hom.rel_id`, `comp_id`, `UniformSpace.Core.refl`
`image` 📖	CompOp	34 math math: `Fintype.all_card_le_rel_image_card_iff_exists_injective`, `UniformSpace.closure_subset_image`, `IsClosed.relImage_of_isCompact`, `image_subset_iff`, `Set.image_eq`, `image_sUnion`, `image_empty_left`, `Filter.rcomap_sets`, `mem_image`, `image_core_gc`, `image_empty_right`, `image_subset_image_left`, `image_inter_subset`, `image_union`, `image_subset_image`, `self_subset_image`, `image_mono`, `mem_hausdorffEntourage`, `preimage_eq_image`, `Filter.rcomap'_sets`, `image_eq_biUnion`, `image_id`, `IsOpen.relImage`, `inter_dom_subset_preimage_image`, `inter_cod_subset_image_preimage`, `image_univ_right`, `image_inv`, `image_iUnion`, `image_univ_left`, `image_inter_dom`, `image_comp`, `preimage_inv`, `IsClosed.relImage_of_finite`, `image_entourageProd_prod`
`inv` 📖	CompOp	33 math math: `IsWellFounded.inv_of_finiteDimensional`, `IsOpen.relInv`, `IsClosed.relInv`, `inv_comp`, `finiteDimensional_inv`, `InfiniteDimensional.inv`, `isSymm_inv_comp`, `mem_inv`, `RelSeries.head_reverse`, `RelSeries.reverse_reverse`, `Equiv.graph_inv`, `isSymm_comp_inv`, `cod_inv`, `inv_hausdorffEntourage`, `inv_univ`, `symmetrize_subset_inv`, `RelSeries.last_reverse`, `RelSeries.reverse_length`, `RelSeries.reverse_apply`, `inv_eq_self`, `inv_entourageProd`, `inv_inv`, `inv_id`, `inv_eq_self_iff`, `dom_inv`, `infiniteDimensional_inv`, `image_inv`, `inv_empty`, `subset_symmetrize`, `inv_mono`, `instIsSymmInv`, `FiniteDimensional.inv`, `preimage_inv`
`preimage` 📖	CompOp	37 math math: `preimage_univ_right`, `preimage_union`, `preimage_eq_dom_of_cod_subset`, `self_subset_preimage`, `Set.preimage_eq`, `rtendsto'_nhds`, `IsClosed.relPreimage_of_isCompact`, `preimage_eq_biUnion`, `Filter.rtendsto'_def`, `preimage_inter_subset`, `Filter.TotallyBounded.exists_subset_of_mem`, `preimage_comp`, `mem_preimage`, `Filter.HasBasis.filter_totallyBounded_iff`, `IsOpen.relPreimage`, `preimage_inter_cod`, `image_eq_cod_of_dom_subset`, `mem_hausdorffEntourage`, `preimage_mono`, `preimage_eq_image`, `preimage_univ_left`, `preimage_iUnion`, `Filter.rcomap'_sets`, `preimage_entourageProd_prod`, `inter_dom_subset_preimage_image`, `preimage_empty_right`, `IsClosed.relPreimage_of_finite`, `preimage_sUnion`, `preimage_subset_preimage`, `inter_cod_subset_image_preimage`, `Filter.mem_rcomap'`, `UniformSpace.closure_subset_preimage`, `image_inv`, `preimage_subset_preimage_left`, `preimage_id`, `preimage_inv`, `preimage_empty_left`
`restrictDomain` 📖	CompOp	—
`symmetrize` 📖	CompOp	8 math math: `IsTransitiveRel.symmetrizeRel`, `symmetrize_mem_uniformity`, `isSymm_symmetrize`, `symmetrize_subset_inv`, `symmetrize_mono`, `symmetrize_subset_self`, `isTrans_symmetrize`, `subset_symmetrize`
`«term_~[_]_»` 📖	CompOp	—
`«term_○_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cod_empty` 📖	mathematical	—	`cod` `SetRel` `Set.instEmptyCollection` `Set`	—	`Set.ext`
`cod_eq_empty_iff` 📖	mathematical	—	`cod` `Set` `Set.instEmptyCollection` `SetRel`	—	`Set.eq_empty_iff_forall_notMem` `cod_empty`
`cod_inv` 📖	mathematical	—	`cod` `inv` `dom`	—	—
`cod_mono` 📖	mathematical	`SetRel` `Set.instLE`	`Set` `Set.instHasSubset` `cod`	—	—
`cod_univ` 📖	mathematical	—	`cod` `Set.univ`	—	`Set.ext`
`comm` 📖	mathematical	—	`SetRel` `Set.instMembership`	—	`comm_of`
`comp_assoc` 📖	mathematical	—	`comp`	—	`Set.ext`
`comp_empty` 📖	mathematical	—	`comp` `SetRel` `Set.instEmptyCollection`	—	`Set.ext`
`comp_eq_self` 📖	mathematical	—	`comp`	—	`subset_antisymm` `Set.instAntisymmSubset` `comp_subset_self` `left_subset_comp`
`comp_iUnion` 📖	mathematical	—	`comp` `Set.iUnion`	—	`Set.ext`
`comp_id` 📖	mathematical	—	`comp` `id`	—	`Set.ext`
`comp_sUnion` 📖	mathematical	—	`comp` `Set.sUnion` `Set.iUnion` `SetRel` `Set` `Set.instMembership`	—	`Set.ext`
`comp_subset_comp` 📖	mathematical	`SetRel` `Set.instHasSubset`	`comp`	—	—
`comp_subset_comp_left` 📖	mathematical	`SetRel` `Set.instHasSubset`	`comp`	—	`comp_subset_comp` `Set.Subset.rfl`
`comp_subset_comp_right` 📖	mathematical	`SetRel` `Set.instHasSubset`	`comp`	—	`comp_subset_comp` `Set.Subset.rfl`
`comp_subset_self` 📖	mathematical	—	`SetRel` `Set.instHasSubset` `comp`	—	`trans`
`comp_univ` 📖	mathematical	—	`comp` `Set.univ` `setOf` `Set` `Set.instMembership` `dom`	—	`Set.ext`
`core_comp` 📖	mathematical	—	`core` `comp`	—	`Set.ext`
`core_id` 📖	mathematical	—	`core` `id`	—	`Set.ext`
`core_inter` 📖	mathematical	—	`core` `Set` `Set.instInter`	—	`Set.ext`
`core_mono` 📖	mathematical	—	`Monotone` `Set` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `Set.instBooleanAlgebra` `core`	—	`core_subset_core`
`core_subset_core` 📖	mathematical	`Set` `Set.instHasSubset`	`core`	—	—
`core_union_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.instUnion` `core`	—	`Monotone.le_map_sup` `core_mono`
`core_univ` 📖	mathematical	—	`core` `Set.univ`	—	`Set.ext`
`dom_empty` 📖	mathematical	—	`dom` `SetRel` `Set.instEmptyCollection` `Set`	—	`Set.ext`
`dom_eq_empty_iff` 📖	mathematical	—	`dom` `Set` `Set.instEmptyCollection` `SetRel`	—	`Set.eq_empty_iff_forall_notMem` `dom_empty`
`dom_inv` 📖	mathematical	—	`dom` `inv` `cod`	—	—
`dom_mono` 📖	mathematical	`SetRel` `Set.instLE`	`Set` `Set.instHasSubset` `dom`	—	—
`dom_univ` 📖	mathematical	—	`dom` `Set.univ`	—	`Set.ext`
`empty_comp` 📖	mathematical	—	`comp` `SetRel` `Set.instEmptyCollection`	—	`Set.ext`
`exists_eq_singleton_of_prod_subset_id` 📖	mathematical	`Set.Nonempty` `Set` `Set.instHasSubset` `SProd.sprod` `Set.instSProd` `id`	`Set.instSingletonSet`	—	—
`exists_graph_eq_iff` 📖	mathematical	—	`ExistsUnique` `SetRel` `Function.graph` `Set.instMembership`	—	`Set.ext` `ExistsUnique.unique` `ExistsUnique.exists`
`iUnion_comp` 📖	mathematical	—	`comp` `Set.iUnion`	—	`Set.ext`
`id_comp` 📖	mathematical	—	`comp` `id`	—	`Set.ext`
`id_subset` 📖	mathematical	—	`SetRel` `Set.instHasSubset` `id`	—	`rfl`
`id_subset_iff` 📖	mathematical	—	`SetRel` `Set.instHasSubset` `id` `IsRefl`	—	`id_subset`
`image_comp` 📖	mathematical	—	`image` `comp`	—	`Set.ext`
`image_core_gc` 📖	mathematical	—	`GaloisConnection` `Set` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `Set.instBooleanAlgebra` `image` `core`	—	`image_subset_iff`
`image_empty_left` 📖	mathematical	—	`image` `SetRel` `Set.instEmptyCollection` `Set`	—	`Set.ext`
`image_empty_right` 📖	mathematical	—	`image` `Set` `Set.instEmptyCollection`	—	`Set.ext`
`image_eq_biUnion` 📖	mathematical	—	`image` `Set.iUnion` `Set` `Set.instMembership` `setOf` `SetRel`	—	`Set.ext`
`image_eq_cod_of_dom_subset` 📖	mathematical	`Set` `Set.instHasSubset` `cod`	`preimage` `dom`	—	`Set.ext`
`image_iUnion` 📖	mathematical	—	`image` `Set.iUnion`	—	`Set.ext`
`image_id` 📖	mathematical	—	`image` `id`	—	`Set.ext`
`image_inter_dom` 📖	mathematical	—	`image` `Set` `Set.instInter` `dom`	—	`Set.ext`
`image_inter_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `image` `Set.instInter`	—	`Monotone.map_inf_le` `image_mono`
`image_inv` 📖	mathematical	—	`image` `inv` `preimage`	—	—
`image_mono` 📖	mathematical	—	`Monotone` `Set` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `Set.instBooleanAlgebra` `image`	—	`image_subset_image`
`image_sUnion` 📖	mathematical	—	`image` `Set.sUnion` `Set.iUnion` `Set` `Set.instMembership`	—	`Set.ext`
`image_subset_iff` 📖	mathematical	—	`Set` `Set.instHasSubset` `image` `core`	—	—
`image_subset_image` 📖	mathematical	`Set` `Set.instHasSubset`	`image`	—	—
`image_subset_image_left` 📖	mathematical	`SetRel` `Set.instHasSubset`	`Set` `image`	—	—
`image_union` 📖	mathematical	—	`image` `Set` `Set.instUnion`	—	`Set.ext`
`image_univ_left` 📖	mathematical	`Set.Nonempty`	`image` `Set.univ`	—	`Set.ext`
`image_univ_right` 📖	mathematical	—	`image` `Set.univ` `cod`	—	`Set.ext`
`instIsIrreflSetOfProdMatch_1PropOfIrrefl` 📖	mathematical	—	`IsIrrefl` `setOf`	—	—
`instIsSymmInv` 📖	mathematical	—	`IsSymm` `inv`	—	`inv_eq_self`
`instIsTransSetOfProdMatch_1PropOfIsTrans` 📖	mathematical	—	`IsTrans` `setOf`	—	—
`inter_cod_subset_image_preimage` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.instInter` `cod` `image` `preimage`	—	—
`inter_dom_subset_preimage_image` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.instInter` `dom` `preimage` `image`	—	—
`inv_comp` 📖	mathematical	—	`inv` `comp`	—	`Set.ext`
`inv_empty` 📖	mathematical	—	`inv` `SetRel` `Set.instEmptyCollection`	—	—
`inv_eq_self` 📖	mathematical	—	`inv`	—	`Set.ext` `comm`
`inv_eq_self_iff` 📖	mathematical	—	`inv` `IsSymm`	—	`inv_eq_self`
`inv_id` 📖	mathematical	—	`inv` `id`	—	`Set.ext`
`inv_inv` 📖	mathematical	—	`inv`	—	—
`inv_mono` 📖	mathematical	`SetRel` `Set.instHasSubset`	`inv`	—	—
`inv_univ` 📖	mathematical	—	`inv` `Set.univ`	—	—
`irrefl` 📖	mathematical	—	`SetRel` `Set.instMembership`	—	`irrefl_of`
`isRefl_iInter` 📖	mathematical	`IsRefl`	`Set.iInter`	—	`IsRefl.sInter`
`isRefl_inter` 📖	mathematical	—	`IsRefl` `SetRel` `Set.instInter`	—	`rfl`
`isRefl_mono` 📖	mathematical	`SetRel` `Set.instHasSubset`	`IsRefl`	—	`rfl`
`isRefl_preimage` 📖	mathematical	—	`IsRefl` `Set.preimage`	—	`rfl`
`isRefl_univ` 📖	mathematical	—	`IsRefl` `Set.univ`	—	—
`isSymm_comp_inv` 📖	mathematical	—	`IsSymm` `comp` `inv`	—	—
`isSymm_comp_self` 📖	mathematical	—	`IsSymm` `comp`	—	`inv_eq_self` `isSymm_comp_inv`
`isSymm_empty` 📖	mathematical	—	`IsSymm` `SetRel` `Set.instEmptyCollection`	—	—
`isSymm_iInter` 📖	mathematical	`IsSymm`	`Set.iInter`	—	`IsSymm.sInter`
`isSymm_id` 📖	mathematical	—	`IsSymm` `id`	—	—
`isSymm_image` 📖	mathematical	—	`IsSymm` `Set.image`	—	`symm`
`isSymm_inter` 📖	mathematical	—	`IsSymm` `SetRel` `Set.instInter`	—	`symm`
`isSymm_inv_comp` 📖	mathematical	—	`IsSymm` `comp` `inv`	—	`isSymm_comp_inv`
`isSymm_preimage` 📖	mathematical	—	`IsSymm` `Set.preimage`	—	`symm`
`isSymm_symmetrize` 📖	mathematical	—	`IsSymm` `symmetrize`	—	—
`isSymm_univ` 📖	mathematical	—	`IsSymm` `Set.univ`	—	—
`isTrans_empty` 📖	mathematical	—	`IsTrans` `SetRel` `Set.instEmptyCollection`	—	—
`isTrans_iInter` 📖	mathematical	`IsTrans`	`Set.iInter`	—	`IsTrans.sInter`
`isTrans_id` 📖	mathematical	—	`IsTrans` `id`	—	—
`isTrans_iff_comp_subset_self` 📖	mathematical	—	`IsTrans` `SetRel` `Set.instHasSubset` `comp`	—	`comp_subset_self`
`isTrans_inter` 📖	mathematical	—	`IsTrans` `SetRel` `Set.instInter`	—	`trans`
`isTrans_preimage` 📖	mathematical	—	`IsTrans` `Set.preimage`	—	`trans`
`isTrans_singleton` 📖	mathematical	—	`IsTrans` `SetRel` `Set.instSingletonSet`	—	—
`isTrans_symmetrize` 📖	mathematical	—	`IsTrans` `symmetrize`	—	`trans`
`isTrans_univ` 📖	mathematical	—	`IsTrans` `Set.univ`	—	—
`left_subset_comp` 📖	mathematical	—	`SetRel` `Set.instHasSubset` `comp`	—	`comp_id` `comp_subset_comp_right` `id_subset`
`mem_cod` 📖	mathematical	—	`Set` `Set.instMembership` `cod` `SetRel`	—	—
`mem_comp` 📖	mathematical	—	`SetRel` `Set.instMembership` `comp`	—	—
`mem_core` 📖	mathematical	—	`Set` `Set.instMembership` `core`	—	—
`mem_dom` 📖	mathematical	—	`Set` `Set.instMembership` `dom` `SetRel`	—	—
`mem_id` 📖	mathematical	—	`SetRel` `Set.instMembership` `id`	—	—
`mem_image` 📖	mathematical	—	`Set` `Set.instMembership` `image` `SetRel`	—	—
`mem_inv` 📖	mathematical	—	`SetRel` `Set.instMembership` `inv`	—	—
`mem_preimage` 📖	mathematical	—	`Set` `Set.instMembership` `preimage` `SetRel`	—	—
`preimage_comp` 📖	mathematical	—	`preimage` `comp`	—	`Set.ext`
`preimage_empty_left` 📖	mathematical	—	`preimage` `SetRel` `Set.instEmptyCollection` `Set`	—	`Set.ext`
`preimage_empty_right` 📖	mathematical	—	`preimage` `Set` `Set.instEmptyCollection`	—	`Set.ext`
`preimage_eq_biUnion` 📖	mathematical	—	`preimage` `Set.iUnion` `Set` `Set.instMembership` `setOf` `SetRel`	—	`Set.ext`
`preimage_eq_dom_of_cod_subset` 📖	mathematical	`Set` `Set.instHasSubset` `cod`	`preimage` `dom`	—	`Set.ext`
`preimage_eq_image` 📖	mathematical	—	`preimage` `image`	—	`preimage_inv` `inv_eq_self`
`preimage_iUnion` 📖	mathematical	—	`preimage` `Set.iUnion`	—	`Set.ext`
`preimage_id` 📖	mathematical	—	`preimage` `id`	—	`Set.ext`
`preimage_inter_cod` 📖	mathematical	—	`preimage` `Set` `Set.instInter` `cod`	—	`Set.ext`
`preimage_inter_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `preimage` `Set.instInter`	—	`Monotone.map_inf_le` `preimage_mono`
`preimage_inv` 📖	mathematical	—	`preimage` `inv` `image`	—	—
`preimage_mono` 📖	mathematical	—	`Monotone` `Set` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `Set.instBooleanAlgebra` `preimage`	—	`preimage_subset_preimage`
`preimage_sUnion` 📖	mathematical	—	`preimage` `Set.sUnion` `Set.iUnion` `Set` `Set.instMembership`	—	`Set.ext`
`preimage_subset_preimage` 📖	mathematical	`Set` `Set.instHasSubset`	`preimage`	—	—
`preimage_subset_preimage_left` 📖	mathematical	`SetRel` `Set.instHasSubset`	`Set` `preimage`	—	—
`preimage_union` 📖	mathematical	—	`preimage` `Set` `Set.instUnion`	—	`Set.ext`
`preimage_univ_left` 📖	mathematical	`Set.Nonempty`	`preimage` `Set.univ`	—	`Set.ext`
`preimage_univ_right` 📖	mathematical	—	`preimage` `Set.univ` `dom`	—	`Set.ext`
`prodMk_mem_comp` 📖	mathematical	`SetRel` `Set.instMembership`	`comp`	—	—
`prod_comp_prod` 📖	mathematical	—	`comp` `SProd.sprod` `Set` `Set.instSProd` `Disjoint` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `Set.instBooleanAlgebra` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra` `Set.instEmptyCollection`	—	`prod_comp_prod_of_disjoint` `prod_comp_prod_of_inter_nonempty` `Set.not_disjoint_iff_nonempty_inter`
`prod_comp_prod_of_disjoint` 📖	mathematical	`Disjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `Set.instBooleanAlgebra` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra`	`comp` `SProd.sprod` `Set.instSProd` `SetRel` `Set.instEmptyCollection`	—	`Set.eq_empty_of_forall_notMem` `Set.disjoint_left`
`prod_comp_prod_of_inter_nonempty` 📖	mathematical	`Set.Nonempty` `Set` `Set.instInter`	`comp` `SProd.sprod` `Set.instSProd`	—	`Set.ext`
`prod_subset_comm` 📖	mathematical	—	`Set` `Set.instHasSubset` `SProd.sprod` `Set.instSProd`	—	`inv_eq_self` `inv.eq_1` `Set.image_subset_iff` `Set.image_swap_prod`
`refl` 📖	mathematical	—	`SetRel` `Set.instMembership`	—	`refl_of`
`rfl` 📖	mathematical	—	`SetRel` `Set.instMembership`	—	`refl`
`right_subset_comp` 📖	mathematical	—	`SetRel` `Set.instHasSubset` `comp`	—	`id_comp` `comp_subset_comp_left` `id_subset`
`sUnion_comp` 📖	mathematical	—	`comp` `Set.sUnion` `Set.iUnion` `SetRel` `Set` `Set.instMembership`	—	`Set.ext`
`self_subset_image` 📖	mathematical	—	`Set` `Set.instHasSubset` `image`	—	`rfl`
`self_subset_preimage` 📖	mathematical	—	`Set` `Set.instHasSubset` `preimage`	—	`rfl`
`subset_iterate_comp` 📖	mathematical	—	`SetRel` `Set.instHasSubset` `Nat.iterate` `comp`	—	`Set.Subset.rfl` `HasSubset.Subset.trans` `Set.instIsTransSubset` `right_subset_comp`
`subset_symmetrize` 📖	mathematical	—	`SetRel` `Set.instHasSubset` `symmetrize` `inv`	—	`Set.subset_inter_iff`
`symmetrize_mono` 📖	mathematical	`SetRel` `Set.instHasSubset`	`symmetrize`	—	`Set.inter_subset_inter` `Set.preimage_mono`
`symmetrize_subset_inv` 📖	mathematical	—	`SetRel` `Set.instHasSubset` `symmetrize` `inv`	—	`Set.inter_subset_right`
`symmetrize_subset_self` 📖	mathematical	—	`SetRel` `Set.instHasSubset` `symmetrize`	—	`Set.inter_subset_left`
`trans` 📖	—	`SetRel` `Set.instMembership`	—	—	`trans_of`
`univ_comp` 📖	mathematical	—	`comp` `Set.univ` `setOf` `Set` `Set.instMembership` `cod`	—	`Set.ext`

SetRel.IsRefl

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	mathematical	—	`SetRel.IsRefl` `SetRel.comp`	—	`SetRel.rfl`
`sInter` 📖	mathematical	`SetRel.IsRefl`	`Set.sInter`	—	—

SetRel.IsSymm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sInter` 📖	mathematical	`SetRel.IsSymm`	`Set.sInter`	—	—

SetRel.IsTrans

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sInter` 📖	mathematical	`SetRel.IsTrans`	`Set.sInter`	—	`IsTrans.trans`

SimpleGraph.TripartiteFromTriangles

Definitions

Name	Category	Theorems
`Rel` 📖	CompData	3 math math: `rel_iff`, `rel_irrefl`, `rel_symm`

Sym2

Definitions

Name	Category	Theorems
`Rel` 📖	CompData	7 math math: `eq`, `out_fst_mem`, `Rel.is_equivalence`, `rel_iff'`, `rel_iff`, `exact`, `out_snd_mem`

SymmetricPower

Definitions

Name	Category	Theorems
`Rel` 📖	CompData	—

TensorAlgebra

Definitions

Name	Category	Theorems
`Rel` 📖	CompData	2 math math: `ι_def`, `ringQuot_mkAlgHom_freeAlgebra_ι_eq_ι`

TopCat.GlueData

Definitions

Name	Category	Theorems
`Rel` 📖	MathDef	2 math math: `rel_equiv`, `ι_eq_iff_rel`

UniversalEnvelopingAlgebra

Definitions

Name	Category	Theorems
`Rel` 📖	CompData	—

ValuativeRel

Definitions

Name	Category	Theorems
`Rel` 📖	MathDef	—

(root)

Definitions

Name	Category	Theorems
`Rel` 📖	CompOp	—
`SetRel` 📖	CompOp	120 math math: `Fintype.all_card_le_rel_image_card_iff_exists_injective`, `UniformSpace.mem_uniformity_ofCore_iff`, `isTransitiveRel_singleton`, `Dynamics.coverEntropyInfEntourage_antitone`, `SetRel.mem_comp`, `monotone_hausdorffEntourage`, `IsTransitiveRel.inter`, `uniformity_hasBasis_closed`, `Filter.HasBasis.mem_uniformity_iff`, `entourageProd_subset`, `RelSeries.rel_or_eq_of_le`, `Filter.HasBasis.cauchySeq_iff`, `SetRel.image_empty_left`, `UniformSpace.ball_eq_of_symmetry`, `SetRel.sUnion_comp`, `SetRel.mem_image`, `UniformSpace.mem_comp_of_mem_ball`, `Dynamics.netEntropyEntourage_antitone`, `SetRel.preimage_eq_biUnion`, `CauchyFilter.mem_uniformity`, `Function.graph_injective`, `SetRel.left_subset_comp`, `right_subset_compRel`, `idRel_subset`, `uniformity_hasBasis_closure`, `SetRel.prod_comp_prod_of_disjoint`, `SetRel.right_subset_comp`, `SetRel.comp_empty`, `Filter.HasBasis.cauchySeq_iff'`, `SetRel.comp_sUnion`, `SetRel.mem_inv`, `Filter.HasBasis.uniformity_hausdorff`, `discreteUniformity_iff_setRelId_mem_uniformity`, `Dynamics.coverMincard_antitone`, `Dynamics.netMaxcard_antitone`, `EMetric.mem_hausdorffEntourage_of_hausdorffEdist_lt`, `CategoryTheory.RelCat.Hom.rel_id_apply₂`, `subset_comp_self`, `isTransitiveRel_iff_comp_subset_self`, `discreteUniformity_iff_relId_mem_uniformity`, `nhds_nhds_eq_uniformity_uniformity_prod`, `subset_iterate_compRel`, `SetRel.mem_preimage`, `CauchyFilter.basis_uniformity`, `Dynamics.mem_dynEntourage`, `SetRel.irrefl`, `DiscreteUniformity.relId_mem_uniformity`, `CauchyFilter.monotone_gen`, `Dynamics.dynEntourage_comp_subset`, `UniformSpace.hasBasis_nhds`, `SetRel.rfl`, `uniformity_hasBasis_open_symmetric`, `mem_hausdorffEntourage`, `SetRel.symmetrize_subset_inv`, `UniformSpace.uniformSpace_eq_bot`, `Dynamics.coverEntropyEntourage_antitone`, `Filter.HasBasis.totallyBounded_iff`, `SetRel.comp_subset_self`, `SetRel.mem_cod`, `left_subset_compRel`, `SetRel.isRefl_inter`, `discreteUniformity_iff_idRel_mem_uniformity`, `SetRel.mem_id`, `mem_entourageProd`, `SetRel.isSymm_inter`, `UniformSpace.mem_comp_comp`, `symmetrizeRel_subset_self`, `CategoryTheory.RelCat.Hom.rel_comp_apply₂`, `SetRel.isSeparated_insert_of_notMem`, `SetRel.id_subset_iff`, `SetRel.id_subset`, `Filter.HasBasis.cauchy_iff`, `DiscreteUniformity.idRel_mem_uniformity`, `SetRel.symmetrize_subset_self`, `SetRel.image_eq_biUnion`, `RelSeries.toList_chain'`, `IsSymmetricRel.mk_mem_comm`, `mem_compRel`, `RelSeries.last_map`, `SetRel.comm`, `Metric.mem_hausdorffEntourage_of_hausdorffEDist_lt`, `SetRel.dom_eq_empty_iff`, `RelSeries.eraseLast_last_rel_last`, `Function.mem_graph`, `RelSeries.rel_of_lt`, `RelSeries.head_map`, `SetRel.isTrans_inter`, `SetRel.isTrans_empty`, `singleton_mem_hausdorffEntourage`, `RelSeries.map_apply`, `nhds_eq_uniformity_prod`, `SetRel.refl`, `SetRel.isSymm_empty`, `RelSeries.step`, `Dynamics.netEntropyInfEntourage_antitone`, `Dynamics.dynEntourage_antitone`, `SetRel.mem_filter_prod_comm`, `SetRel.inv_empty`, `SetRel.exists_graph_eq_iff`, `SetRel.empty_comp`, `IsUltraUniformity.hasBasis`, `SetRel.subset_symmetrize`, `SetRel.dom_empty`, `isTransitiveRel_empty`, `UniformSpace.hasBasis_symmetric`, `lift_nhds_right`, `nhds_basis_uniformity`, `SetRel.cod_eq_empty_iff`, `SetRel.isTrans_singleton`, `SetRel.mem_dom`, `uniformity_hasBasis_open`, `RelSeries.isChain_toList`, `SetRel.cod_empty`, `IsSymmetricRel.inter`, `IsTransitiveRel.comp_subset_self`, `Filter.HasBasis.uniformSpace_eq_bot`, `SetRel.subset_iterate_comp`, `Dynamics.dynEntourage_monotone`, `SetRel.isTrans_iff_comp_subset_self`, `SetRel.preimage_empty_left`

---

← Back to Index