map_fundamentalDomain — Mathlib

English

Under a linear isomorphism f: E ≃ₗ[K] F, the image of the fundamental domain of b is the fundamental domain of the mapped basis b.map f.

Русский

Пусть f: E \\to F — линейное изоморфизм. Образ фундаментальной области b равен фундаментальной области базиса, полученного при отображении f: b.map f.

LaTeX

$$$ f''\\operatorname{fundamentalDomain}(b) = \\operatorname{fundamentalDomain}(b.map\,f) $$$

Lean4

theorem map_fundamentalDomain {F : Type*} [NormedAddCommGroup F] [NormedSpace K F] (f : E ≃ₗ[K] F) :
    f '' (fundamentalDomain b) = fundamentalDomain (b.map f) :=
  by
  ext x
  rw [mem_fundamentalDomain, Basis.map_repr, LinearEquiv.trans_apply, ← mem_fundamentalDomain,
    show f.symm x = f.toEquiv.symm x by rfl, ← Set.mem_image_equiv]
  rfl

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