English
If E is an equivalence between index sets σ and τ, renaming the index in a CFilter by E yields a canonical isomorphism between CFilter α σ and CFilter α τ, given by F ↦ F.ofEquiv E (and vice versa via E.symm).
Русский
Пусть E — биекция между множествами индексов σ и τ. Перекраска основания CFilter по E дает каноническое изоморождение между CFilter α σ и CFilter α τ, задаваемое F ↦ F.ofEquiv E (и обратное через E.symm).
LaTeX
$$$CFilter(\\alpha, \\sigma) \\cong CFilter(\\alpha, \\tau)$ via $F \\mapsto F.ofEquiv(E)$ and inverse $G \\mapsto G.ofEquiv(E^{-1})$.$$
Lean4
/-- Map a `CFilter` to an equivalent representation type. -/
def ofEquiv (E : σ ≃ τ) : CFilter α σ → CFilter α τ
| ⟨f, p, g, h₁, h₂⟩ =>
{ f := fun a ↦ f (E.symm a)
pt := E p
inf := fun a b ↦ E (g (E.symm a) (E.symm b))
inf_le_left := fun a b ↦ by simpa using h₁ (E.symm a) (E.symm b)
inf_le_right := fun a b ↦ by simpa using h₂ (E.symm a) (E.symm b) }
