of_equiv — Mathlib

English

If G is generated by x, and e is an equivalence between index types, then G is generated by the reindexed family x ∘ e.

Русский

Если G порожден через x и e — эквивалент между индексными множествами, то G порожден через переразнесенный набор x ∘ e.

LaTeX

$$$G\text{ isGeneratedBy } x \Rightarrow \forall {ι'}\ (e:\iota'\simeq \iota),\ G\text{ isGeneratedBy }(\lambda i'\mapsto x( e i'))$$$

Lean4

theorem of_equiv {ι' : Type w''} (e : ι' ≃ ι) : G.IsGeneratedBy (fun i' ↦ x (e i')) :=
  by
  rw [isGeneratedBy_iff, ← h.iSup_eq]
  exact Equiv.iSup_congr e (congrFun rfl)

Похожие утверждения