English
Reindexing a basis preserves the parallelepiped; (b.reindex e).parallelepiped = b.parallelepiped.
Русский
Переиндексация базиса сохраняет параллелепипед; параллелеепипед остается тем же.
LaTeX
$$$ (b.reindex\\,e).parallelepiped = b.parallelepiped $.$$
Lean4
/-- The parallelepiped spanned by a basis, as a compact set with nonempty interior. -/
def parallelepiped (b : Basis ι ℝ E) : PositiveCompacts E
where
carrier := _root_.parallelepiped b
isCompact' :=
IsCompact.image isCompact_Icc
(continuous_finset_sum Finset.univ fun (i : ι) (_H : i ∈ Finset.univ) =>
(continuous_apply i).smul continuous_const)
interior_nonempty' :=
by
suffices H : Set.Nonempty (interior (b.equivFunL.symm.toHomeomorph '' Icc 0 1))
by
dsimp only [_root_.parallelepiped]
convert H
exact (b.equivFun_symm_apply _).symm
have A : Set.Nonempty (interior (Icc (0 : ι → ℝ) 1)) :=
by
rw [← pi_univ_Icc, interior_pi_set (@finite_univ ι _)]
simp only [univ_pi_nonempty_iff, Pi.zero_apply, Pi.one_apply, interior_Icc, nonempty_Ioo, zero_lt_one,
imp_true_iff]
rwa [← Homeomorph.image_interior, image_nonempty]
