inf — Mathlib

English

The infimum of two regular spaces is regular.

Русский

Infimum двух регулярных пространств — регулярное пространство.

LaTeX

$$$\forall X, t_1, t_2: RegularSpace X, RegularSpace X (t_1 \inf t_2)$$$

Lean4

theorem inf {X} {t₁ t₂ : TopologicalSpace X} (h₁ : @RegularSpace X t₁) (h₂ : @RegularSpace X t₂) :
    @RegularSpace X (t₁ ⊓ t₂) := by
  rw [inf_eq_iInf]
  exact regularSpace_iInf (Bool.forall_bool.2 ⟨h₂, h₁⟩)

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