English
Let F be a realizer on α with index σ and let E be an equivalence between σ and τ. Then one can transport F along E to obtain a new realizer on α with index τ, denoted F.ofEquiv E, whose data are obtained by relabeling indices via E and transporting the underlying neighborhood data accordingly.
Русский
Пусть F — реализатор на α с индексами σ, а E — эквивалентность σ и τ. Тогда можно перенести F вдоль E и получить новый реализатор на α с индексами τ, обозначаемый F.ofEquiv E; данные строятся путем перенумерации индексов через E и переноса связанной структуры окрестностей.
LaTeX
$$$ (F\mathrm{ofEquiv} E).\sigma = \tau \quad \text{и} \quad (F\mathrm{ofEquiv} E).\mathrm{F}(t) = F.\mathrm{F}(E.\mathrm{symm}(t)) \text{ for all } t \in \tau. $$$$
Lean4
/-- Replace the representation type of a `Ctop` realizer. -/
def ofEquiv (F : Realizer α) (E : F.σ ≃ τ) : Realizer α :=
⟨τ, F.F.ofEquiv E,
ext' fun a s ↦
F.mem_nhds.trans <| ⟨fun ⟨s, h⟩ ↦ ⟨E s, by simpa using h⟩, fun ⟨t, h⟩ ↦ ⟨E.symm t, by simpa using h⟩⟩⟩
