Congruence

📁 Source: Mathlib/Topology/MetricSpace/Congruence.lean

Statistics

Metric	Count
Definitions `Congruence`, `Congruent`, `«term_≅_»`	3
Theorems `comp_dilation`, `comp_left`, `comp_left_iff`, `comp_right`, `comp_right_iff`, `dist_eq`, `edist_eq`, `index_equiv`, `index_map`, `nndist_eq`, `of_dist_eq`, `of_edist_eq`, `of_nndist_eq`, `of_pairwise_dist_eq`, `of_pairwise_edist_eq`, `of_pairwise_nndist_eq`, `of_subsingleton_index`, `pairwise_dist_eq`, `pairwise_edist_eq`, `pairwise_nndist_eq`, `refl`, `trans`, `congruent_comm`, `congruent_iff_dist_eq`, `congruent_iff_edist_eq`, `congruent_iff_nndist_eq`, `congruent_iff_pairwise_dist_eq`, `congruent_iff_pairwise_edist_eq`, `congruent_iff_pairwise_nndist_eq`	29
Total	32

CategoryTheory

Definitions

Name	Category	Theorems
`Congruence` 📖	CompData	4 math math: `HomotopicalAlgebra.BifibrantObject.instCongruenceHomRel`, `Quotient.compClosure.congruence`, `homotopy_congruence`, `Functor.congruence_homRel`

Congruent

Definitions

Name	Category	Theorems
`«term_≅_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_dilation` 📖	mathematical	`Congruent` `Dilation.ratio`	`DFunLike.coe`	—	`Dilation.edist_eq`
`comp_left` 📖	—	`Isometry` `Congruent`	—	—	`trans`
`comp_left_iff` 📖	mathematical	`Isometry`	`Congruent`	—	`trans` `comp_right` `refl` `comp_left`
`comp_right` 📖	—	`Isometry` `Congruent`	—	—	`trans` `symm`
`comp_right_iff` 📖	mathematical	`Isometry`	`Congruent`	—	`congruent_comm` `comp_left_iff`
`dist_eq` 📖	mathematical	`Congruent` `PseudoMetricSpace.toPseudoEMetricSpace`	`Dist.dist` `PseudoMetricSpace.toDist`	—	`congruent_iff_dist_eq`
`edist_eq` 📖	mathematical	`Congruent`	`EDist.edist` `PseudoEMetricSpace.toEDist`	—	`congruent_iff_edist_eq`
`index_equiv` 📖	mathematical	—	`Congruent` `DFunLike.coe` `EquivLike.toFunLike`	—	`EquivLike.apply_coe_symm_apply` `edist_eq` `index_map`
`index_map` 📖	—	`Congruent`	—	—	`edist_eq`
`nndist_eq` 📖	mathematical	`Congruent` `PseudoMetricSpace.toPseudoEMetricSpace`	`NNDist.nndist` `PseudoMetricSpace.toNNDist`	—	`congruent_iff_nndist_eq`
`of_dist_eq` 📖	mathematical	`Dist.dist` `PseudoMetricSpace.toDist`	`Congruent` `PseudoMetricSpace.toPseudoEMetricSpace`	—	`congruent_iff_dist_eq`
`of_edist_eq` 📖	mathematical	`EDist.edist` `PseudoEMetricSpace.toEDist`	`Congruent`	—	`congruent_iff_edist_eq`
`of_nndist_eq` 📖	mathematical	`NNDist.nndist` `PseudoMetricSpace.toNNDist`	`Congruent` `PseudoMetricSpace.toPseudoEMetricSpace`	—	`congruent_iff_nndist_eq`
`of_pairwise_dist_eq` 📖	mathematical	`Pairwise` `Real` `Dist.dist` `PseudoMetricSpace.toDist`	`Congruent` `PseudoMetricSpace.toPseudoEMetricSpace`	—	`congruent_iff_pairwise_dist_eq`
`of_pairwise_edist_eq` 📖	mathematical	`Pairwise` `ENNReal` `EDist.edist` `PseudoEMetricSpace.toEDist`	`Congruent`	—	`congruent_iff_pairwise_edist_eq`
`of_pairwise_nndist_eq` 📖	mathematical	`Pairwise` `NNReal` `NNDist.nndist` `PseudoMetricSpace.toNNDist`	`Congruent` `PseudoMetricSpace.toPseudoEMetricSpace`	—	`congruent_iff_pairwise_nndist_eq`
`of_subsingleton_index` 📖	mathematical	—	`Congruent`	—	`PseudoEMetricSpace.edist_self`
`pairwise_dist_eq` 📖	mathematical	`Congruent` `PseudoMetricSpace.toPseudoEMetricSpace`	`Pairwise` `Real` `Dist.dist` `PseudoMetricSpace.toDist`	—	`congruent_iff_pairwise_dist_eq`
`pairwise_edist_eq` 📖	mathematical	`Congruent`	`Pairwise` `ENNReal` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	`congruent_iff_pairwise_edist_eq`
`pairwise_nndist_eq` 📖	mathematical	`Congruent` `PseudoMetricSpace.toPseudoEMetricSpace`	`Pairwise` `NNReal` `NNDist.nndist` `PseudoMetricSpace.toNNDist`	—	`congruent_iff_pairwise_nndist_eq`
`refl` 📖	mathematical	—	`Congruent`	—	—
`trans` 📖	—	`Congruent`	—	—	—

(root)

Definitions

Name	Category	Theorems
`Congruent` 📖	MathDef	23 math math: `EuclideanGeometry.side_angle_side`, `Congruent.refl`, `congruent_iff_pairwise_edist_eq`, `Congruent.of_edist_eq`, `Congruent.of_nndist_eq`, `Congruent.of_pairwise_nndist_eq`, `Congruent.of_subsingleton_index`, `Congruent.of_pairwise_edist_eq`, `congruent_iff_pairwise_nndist_eq`, `congruent_comm`, `Congruent.comp_right_iff`, `EuclideanGeometry.triangle_congruent_iff_dist_eq`, `EuclideanGeometry.angle_side_angle`, `EuclideanGeometry.angle_angle_side`, `EuclideanGeometry.side_side_side`, `Congruent.of_pairwise_dist_eq`, `congruent_iff_dist_eq`, `congruent_iff_nndist_eq`, `congruent_iff_edist_eq`, `Congruent.of_dist_eq`, `Congruent.comp_left_iff`, `congruent_iff_pairwise_dist_eq`, `Congruent.index_equiv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`congruent_comm` 📖	mathematical	—	`Congruent`	—	`Congruent.symm`
`congruent_iff_dist_eq` 📖	mathematical	—	`Congruent` `PseudoMetricSpace.toPseudoEMetricSpace` `Dist.dist` `PseudoMetricSpace.toDist`	—	`congruent_iff_nndist_eq` `dist_nndist`
`congruent_iff_edist_eq` 📖	mathematical	—	`Congruent` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	—
`congruent_iff_nndist_eq` 📖	mathematical	—	`Congruent` `PseudoMetricSpace.toPseudoEMetricSpace` `NNDist.nndist` `PseudoMetricSpace.toNNDist`	—	`edist_nndist`
`congruent_iff_pairwise_dist_eq` 📖	mathematical	—	`Congruent` `PseudoMetricSpace.toPseudoEMetricSpace` `Pairwise` `Real` `Dist.dist` `PseudoMetricSpace.toDist`	—	—
`congruent_iff_pairwise_edist_eq` 📖	mathematical	—	`Congruent` `Pairwise` `ENNReal` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	`PseudoEMetricSpace.edist_self`
`congruent_iff_pairwise_nndist_eq` 📖	mathematical	—	`Congruent` `PseudoMetricSpace.toPseudoEMetricSpace` `Pairwise` `NNReal` `NNDist.nndist` `PseudoMetricSpace.toNNDist`	—	`edist_nndist`

---

← Back to Index