gc — Mathlib · SciLib

English

There is a Galois connection between the coercion and interior: (↑) ⊣ interior.

Русский

Существует галуазова связь между коэрцией и interior: (↑) ⊣ interior.

LaTeX

$$$\mathrm{gc} : \mathrm{GaloisConnection}( (↑): \mathrm{Opens}(\alpha) \to \mathcal{P}(\alpha), \mathrm{Opens.interior})$$$

Lean4

theorem gc : GaloisConnection ((↑) : Opens α → Set α) Opens.interior := fun U _ =>
  ⟨fun h => interior_maximal h U.isOpen, fun h => le_trans h interior_subset⟩

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