isGenericPoint_iff_forall_closed — Mathlib

English

If S is closed and x ∈ S, then IsGenericPoint x S is equivalent to: for all closed Z with x ∈ Z, S ⊆ Z.

Русский

Если S замкнуто и x ∈ S, тогда IsGenericPoint x S эквивалентно: для всякого замкнутого Z с x ∈ Z, S ⊆ Z.

LaTeX

$$$ (hS : \ IsClosed S) (hxS : x \in S) : IsGenericPoint x S \iff \forall Z : Set \alpha, IsClosed Z \to x \in Z \to S \subseteq Z$$$

Lean4

theorem isGenericPoint_iff_forall_closed (hS : IsClosed S) (hxS : x ∈ S) :
    IsGenericPoint x S ↔ ∀ Z : Set α, IsClosed Z → x ∈ Z → S ⊆ Z :=
  by
  have : closure { x } ⊆ S := closure_minimal (singleton_subset_iff.2 hxS) hS
  simp_rw [IsGenericPoint, subset_antisymm_iff, this, true_and, closure, subset_sInter_iff, mem_setOf_eq, and_imp,
    singleton_subset_iff]

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