exists_le_of_le_sup — Mathlib

English

For any Us: ι → Opens(X), if principalOpen(x) ≤ iSup Us then exists i with principalOpen(x) ≤ Us(i).

Русский

Для любой семейства открытых Us: ι → Opens(X) выполняется: если principalOpen(x) ≤ iSup Us, то существует i, такое что principalOpen(x) ≤ Us(i).

LaTeX

$$$\\operatorname{principalOpen}(x) \\le \\bigvee_{i \\in ι} Us(i) \\Rightarrow \\exists i, \\operatorname{principalOpen}(x) \\le Us(i)$$$

Lean4

theorem exists_le_of_le_sup {ι : Type v} {x : X} (Us : ι → Opens X) (h : principalOpen x ≤ iSup Us) :
    ∃ i : ι, principalOpen x ≤ Us i := by grind [principalOpen_le_iff, Opens.mem_iSup]

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