bijective_iff_dense_range_and_antilipschitz

English

A linear map with closed graph is continuous.

Русский

Линейное отображение с замкнутым графиком непрерывно.

LaTeX

$$$(g.graph$ closed) \Rightarrow (g$ is continuous)$$$

Lean4

theorem bijective_iff_dense_range_and_antilipschitz (f : E →SL[σ] F) :
    Bijective f ↔ (LinearMap.range f).topologicalClosure = ⊤ ∧ ∃ c, AntilipschitzWith c f :=
  by
  refine ⟨fun h ↦ ⟨?eq_top, ?anti⟩, fun ⟨hd, c, hf⟩ ↦ ⟨hf.injective, ?surj⟩⟩
  case eq_top => simpa [SetLike.ext'_iff] using h.2.denseRange.closure_eq
  case anti =>
    refine ⟨_, ContinuousLinearEquiv.ofBijective f ?_ ?_ |>.antilipschitz⟩ <;>
      simp only [LinearMap.range_eq_top, LinearMapClass.ker_eq_bot, h.1, h.2]
  case surj => rwa [← LinearMap.range_eq_top, ← closed_range_of_antilipschitz hf]

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