instHImp — Mathlib

English

Let α be a topological space. The clopen subsets of α form a Heyting algebra; for any two clopen sets s and t, the implication s ⇒ t is defined by the usual Boolean-algebra implication, namely sᶜ ∪ t, and this is again a clopen set.

Русский

Пусть α — топологическое пространство. Множества, открытые и замкнутые одновременно (клоп/Nclopen), образуют булеву алгебру; для любых клопных множеств s и t импликация s ⇒ t задаётся как sᶜ ∪ t и снова является клопным множеством.

LaTeX

$$$\forall s,t \in \mathrm{Clopens}(\alpha):\ (s \Rightarrow t) = s^{c} \cup t\,,$$$

Lean4

instance : HImp (Clopens α) where himp s t := ⟨s ⇨ t, s.isClopen.himp t.isClopen⟩

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