principalOpen_le_iff — Mathlib

English

For any x and open U, the inclusion of principalOpen(x) into U is equivalent to x belonging to U: principalOpen(x) ≤ U iff x ∈ U.

Русский

Для любых x и открытого множества U равносильно: principalOpen(x) ≤ U тогда и только тогда x ∈ U.

LaTeX

$$$\operatorname{principalOpen}(x) \le U \iff x \in U$$$

Lean4

@[simp]
theorem principalOpen_le_iff {x : X} (U : Opens X) : principalOpen x ≤ U ↔ x ∈ U :=
  by
  refine ⟨fun h => h <| self_mem_principalOpen _, fun hx y hy => ?_⟩
  · have := U.isOpen
    rw [IsUpperSet.isOpen_iff_isUpperSet] at this
    exact this hy hx

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