English
A set s is open if and only if, for every x, the image under chartAt(x) of the intersection of the chart's source with s is open in the target space.
Русский
Множество s открыто тогда и только тогда, когда для каждого x образ изображения chartAt(x) от источника чарта ∩ s открыто в целевом пространстве.
LaTeX
$$$\\text{IsOpen}(s) \\iff \\forall x, \\ IsOpen \\big( chartAt(H,x).toFun' ( (chartAt(H,x).source \\cap s) ) \\big)$$$
Lean4
theorem isOpen_iff (s : Set M) : IsOpen s ↔ ∀ x : M, IsOpen <| chartAt H x '' ((chartAt H x).source ∩ s) :=
by
rw [isOpen_iff_of_cover (fun i ↦ (chartAt H i).open_source) (iUnion_source_chartAt H M)]
simp only [(chartAt H _).isOpen_image_iff_of_subset_source inter_subset_left]
