coe_himp — Mathlib

English

For clopen s,t, the underlying set of the clopen implication s ⇨ t equals the Boolean-algebra implication applied to the underlying sets; i.e., ↑(s ⇨ t) = (↑s) ⇨ (↑t).

Русский

Для клопных s,t множество-носитель импликации s ⇨ t равно импликации булевой алгебры на множествах; т. е. ↑(s ⇨ t) = ↑s ⇨ ↑t.

LaTeX

$$$\uparrow (s \Rightarrow t) = s \Rightarrow t \quad (s,t \in \mathrm{Clopens}(\alpha)).$$$

Lean4

@[simp, norm_cast]
theorem coe_himp (s t : Clopens α) : ↑(s ⇨ t) = (s ⇨ t : Set α) :=
  rfl

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