himp — Mathlib

English

The set s ⇨ t (implication of indicator sets) is clopen when s and t are clopen.

Русский

Множество $s \Rightarrow t$ (импликация индикаторных множеств) открыто-замкнуто, если s и t открыто-замкнуты.

LaTeX

$$$\IsClopen(s) \land \IsClopen(t) \Rightarrow \IsClopen(s \Rightarrow t)$$$

Lean4

theorem himp (hs : IsClopen s) (ht : IsClopen t) : IsClopen (s ⇨ t) := by simpa [himp_eq] using ht.union hs.compl

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