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]