nonempty_preirreducible_inter — Mathlib

English

In a PreirreducibleSpace X, if s and t are open and nonempty, then s ∩ t is nonempty.

Русский

В преднеразложимом пространстве X, если s и t открыты и непусты, то s ∩ t непусто.

LaTeX

$$$[\\text{PreirreducibleSpace } X]\\ IsOpen(s) \\to IsOpen(t) \\to s.Nonempty \\to t.Nonempty \\to (s \\cap t).Nonempty$$$

Lean4

theorem nonempty_preirreducible_inter [PreirreducibleSpace X] :
    IsOpen s → IsOpen t → s.Nonempty → t.Nonempty → (s ∩ t).Nonempty := by
  simpa only [univ_inter, univ_subset_iff] using @PreirreducibleSpace.isPreirreducible_univ X _ _ s t

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