English
There is a natural bijection between boundary elements arising from the left boundaryLE and those arising from the right boundaryGE for complementary embeddings; concretely, Subtype e1.BoundaryLE is in bijection with Subtype e2.BoundaryGE via the maps given by of_boundaryLE and of_boundaryGE.
Русский
Существуют естественные взаимно однозначные соответствия между границами слева и справа для комплементарных вложений; конкретно, подмножество BoundaryLE вложения e1 сопоставимо с BoundaryGE вложения e2 через отображения of_boundaryLE и of_boundaryGE.
LaTeX
$$$\\text{Subtype}\\, e_1.BoundaryLE \\cong \\text{Subtype}\\, e_2.BoundaryGE$$$
Lean4
/-- The bijection `Subtype e₁.BoundaryLE ≃ Subtype e₂.BoundaryGE` when
`e₁` and `e₂` are complementary embeddings of complex shapes. -/
noncomputable def equiv : Subtype e₁.BoundaryLE ≃ Subtype e₂.BoundaryGE
where
toFun := fun ⟨i₁, h⟩ => ⟨_, (of_boundaryLE ac h).snd⟩
invFun := fun ⟨i₂, h⟩ => ⟨_, (of_boundaryGE ac h).fst⟩
left_inv := fun ⟨i₁, h⟩ => by
ext
have h' := of_boundaryLE ac h
have h'' := of_boundaryGE ac h'.snd
exact fst_inj h'' h'
right_inv := fun ⟨i₂, h⟩ => by
ext
have h' := of_boundaryGE ac h
have h'' := of_boundaryLE ac h'.fst
exact snd_inj h'' h'
