interior_eq_empty' — Mathlib

English

Dual version: if nhds within dual order Ioi x nonempty for all x, then interior is empty.

Русский

Дуальная версия: если nhds внутри двойственного порядка Ioi x непусто для каждого x, interior пуст.

LaTeX

$$$\\text{IsAntichain}(\\le, s) \\Rightarrow \\operatorname{Int}(s) = \\varnothing$ (в дуальном порядке)$$

Lean4

theorem interior_eq_empty' [∀ x : α, (𝓝[>] x).NeBot] {s : Set α} (hs : IsAntichain (· ≤ ·) s) : interior s = ∅ :=
  have : ∀ x : αᵒᵈ, NeBot (𝓝[<] x) := ‹_›
  hs.to_dual.interior_eq_empty

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