mem_interior — Mathlib

English

For any x and s, x belongs to interior s iff there exists a set t with t ⊆ s, t open, and x ∈ t.

Русский

Для любого x и s: x ∈ interior(s) тогда и только тогда, когда существует открытое множество t с t ⊆ s и x ∈ t.

LaTeX

$$$$ x \in \operatorname{interior}(s) \iff \exists t,\ t \subseteq s \wedge \operatorname{IsOpen}(t) \wedge x \in t $$$$

Lean4

theorem mem_interior : x ∈ interior s ↔ ∃ t ⊆ s, IsOpen t ∧ x ∈ t := by
  simp only [interior, mem_sUnion, mem_setOf_eq, and_assoc, and_left_comm]

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