coe_himp — Mathlib

English

Let S and T be measurable subsets. The embedding preserves the implication operation of the Boolean algebra: the underlying set of S ⇒ T equals the set-theoretic implication of S and T.

Русский

Пусть S и T — измеримые подмножества. Встраивание сохраняет операцию импликации в булевой алгебре: множество, соответствующее S ⇒ T, есть обычная импликация между множествами S и T.

LaTeX

$$$\\uparrow\\bigl(s \\Rightarrow t\\bigr) = (s \\Rightarrow t : \\mathrm{Set} \\alpha)$$$

Lean4

@[simp]
theorem coe_himp (s t : Subtype (MeasurableSet : Set α → Prop)) : ↑(s ⇨ t) = (s ⇨ t : Set α) :=
  rfl

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