himp_mem

Mathlib.Order.Sublocale

URI: https://scilib.ai/kg/mathlib#Sublocale.himp_mem

English

If b ∈ S, then a ⇨ b ∈ S for any a.

Русский

Если b ∈ S, то для любого a выполняется a ⇨ b ∈ S.

LaTeX

$$$b \in S \Rightarrow a \Rightarrow b \in S$$$

Lean4

theorem himp_mem (hb : b ∈ S) : a ⇨ b ∈ S :=
  S.himp_mem' _ _ hb

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru