isOpen_mk — Mathlib

English

In the bespoke topology defined by a predicate p and accompanying data h1, h2, h3, a set s is open exactly when p(s) holds.

Русский

В топологии, заданной предикатом p и данными h1, h2, h3, множество s открыто тогда, когда выполняется p(s).

LaTeX

$$$\IsOpen_{\langle p,h_1,h_2,h_3\rangle}(s) \iff p(s)$$$

Lean4

theorem isOpen_mk {p h₁ h₂ h₃} : IsOpen[⟨p, h₁, h₂, h₃⟩] s ↔ p s :=
  Iff.rfl

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