interior_eq_empty — Mathlib

English

If s is an antichain in a poset with a rich local structure (nhdsWithin x Iio x nonempty for all x), then the interior of s is empty.

Русский

Если s антинепрерывно по частично упорядоченному множеству и для каждого x выполняется непустость соседей ниже x, то interior(s) пуст.

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 = ∅ :=
  by
  refine eq_empty_of_forall_notMem fun x hx ↦ ?_
  have : ∀ᶠ y in 𝓝 x, y ∈ s := mem_interior_iff_mem_nhds.1 hx
  rcases this.exists_lt with ⟨y, hyx, hys⟩
  exact hs hys (interior_subset hx) hyx.ne hyx.le

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