coe_himp — Mathlib

English

The underlying set of the implication operation equals the Boolean algebra implication on underlying sets.

Русский

Подмножество импликации соответствует импликации булевой алгебры на подмножества.

LaTeX

$$$$ (s \\Rightarrow t) \\text{ with underlying set } = \\mathrm{himp}(s,t) \\text{ on } (α \\to M). $$$$

Lean4

@[simp, norm_cast]
theorem coe_himp (s t : L.DefinableSet A α) : ↑(s ⇨ t) = (s ⇨ t : Set (α → M)) :=
  rfl

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