English
The symmetry of a model-with-corners yields a valid partial equivalence, providing a well-behaved two-sided inverse between spaces.
Π ΡΡΡΠΊΠΈΠΉ
Π‘ΠΈΠΌΠΌΠ΅ΡΡΠΈΡ ΠΌΠΎΠ΄Π΅Π»ΠΈ Ρ ΡΠ³Π»Π°ΠΌΠΈ ΠΎΠ±ΡΠ°Π·ΡΠ΅Ρ ΠΊΠΎΡΡΠ΅ΠΊΡΠ½ΠΎΠ΅ ΡΠ°ΡΡΠΈΡΠ½ΠΎΠ΅ ΡΠΊΠ²Π°Π»Π΅Π½ΡΠ½ΠΎΠ΅ ΠΎΡΠΎΠ±ΡΠ°ΠΆΠ΅Π½ΠΈΠ΅, ΠΎΠ±Π΅ΡΠΏΠ΅ΡΠΈΠ²Π°Ρ Π²Π·Π°ΠΈΠΌΠ½ΠΎ ΠΎΠ΄Π½ΠΎΠ·Π½Π°ΡΠ½ΠΎΠ΅ ΠΎΡΠΎΠ±ΡΠ°ΠΆΠ΅Π½ΠΈΠ΅ ΠΌΠ΅ΠΆΠ΄Ρ Π΄Π²ΡΠΌΡ ΠΏΡΠΎΡΡΡΠ°Π½ΡΡΠ²Π°ΠΌΠΈ.
LaTeX
$$$\\text{ModelWithCorners}.symm : PartialEquiv E H$$$
Lean4
@[scoped macro Manifold.Β«termπ(_)Β»]
public meta def Β«_aux_Mathlib_Geometry_Manifold_IsManifold_Basic___macroRules_Manifold_termπ(_)_1Β» : Macroβ := fun
| `(π($π)) => ``(modelWithCornersSelf $π $π)
| _ => no_error_if_unused% throwβ Lean.Macro.Exception.unsupportedSyntaxβ
