interior_extChartAt_target_nonempty

English

The interior of the target is nonempty.

Русский

Внутренняя часть целевой области непустая.

LaTeX

$$$ \\operatorname{interior}((extChartAt I x).target) \\neq \\emptyset$$$

Lean4

theorem interior_extChartAt_target_nonempty (x : M) : (interior (extChartAt I x).target).Nonempty :=
  by
  by_contra! H
  have := extChartAt_target_subset_closure_interior (mem_extChartAt_target (I := I) x)
  simp only [H, closure_empty, mem_empty_iff_false] at this

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