mem_interior_iff — Mathlib

English

If two sets s and t are almost equal near x, then x is in the interior of s if and only if x is in the interior of t.

Русский

Если множества s и t совпадают почти рядом с x, тогда x ∈ interior(s) тогда и только тогда, когда x ∈ interior(t).

LaTeX

$$$$ s =^\\!\\![\\mathcal{N}(x)] t \\quad \\Rightarrow \\\\ x \\in \\operatorname{int}(s) \\iff x \\in \\operatorname{int}(t) $$$$

Lean4

theorem mem_interior_iff {x : α} {s t : Set α} (hst : s =ᶠ[𝓝 x] t) : x ∈ interior s ↔ x ∈ interior t :=
  ⟨fun h ↦ hst.mem_interior h, fun h ↦ hst.symm.mem_interior h⟩

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