instDistribLatticeOfT2Space — Mathlib

English

If α is a T2 space, then the compact subsets form a distributive lattice under union and intersection.

Русский

Если α — пространство T2, то компактные подмножества образуют распределимую решётку относительно объединения и пересечения.

LaTeX

$$$\text{instance: DistribLattice}(\mathrm{Compacts}\,\alpha)$ for [T2Space α].$$

Lean4

instance [T2Space α] : DistribLattice (Compacts α) :=
  SetLike.coe_injective.distribLattice _ (fun _ _ => rfl) fun _ _ => rfl

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