Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-14 11:12 936eb7ee

View on Github →

feat(analysis/normed_space/finite_dimension): a finite dimensional affine subspace is closed (#13440)

Estimated changes

Modified src/analysis/normed_space/add_torsor.lean

added theorem affine_subspace.is_closed_direction_iff

Modified src/analysis/normed_space/finite_dimension.lean

added theorem affine_equiv.coe_to_homeomorph_of_finite_dimensional

added theorem affine_equiv.coe_to_homeomorph_of_finite_dimensional_symm

added theorem affine_equiv.continuous_of_finite_dimensional

added def affine_equiv.to_homeomorph_of_finite_dimensional

modified theorem affine_map.continuous_of_finite_dimensional

added theorem affine_subspace.closed_of_finite_dimensional