gc_lowerClosure_coe — Mathlib

English

The lower closure operator and the coercion from sets to lower sets form a Galois connection.

Русский

Оператор нижнего замыкания и отображение из множеств в нижние множества образуют галуа‑связь.

LaTeX

$$GaloisConnection (lowerClosure : Set α → LowerSet α) (↑)$$

Lean4

theorem gc_lowerClosure_coe : GaloisConnection (lowerClosure : Set α → LowerSet α) (↑) := fun _s _t ↦ lowerClosure_le

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