inf — Mathlib

English

A set s has a compact superset if and only if closure(s) is compact.

Русский

Существует компактное надмножество K, содержащее s, тогда и только тогда closure(s) компактно.

LaTeX

$$(∃ K, IsCompact K ∧ s ⊆ K) ⇔ IsCompact(closure(s))$$

Lean4

protected theorem inf {X : Type*} {t₁ t₂ : TopologicalSpace X} (h₁ : @R1Space X t₁) (h₂ : @R1Space X t₂) :
    @R1Space X (t₁ ⊓ t₂) := by
  rw [inf_eq_iInf]
  apply R1Space.iInf
  simp [*]

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