map_himp_apply

Mathlib.Order.Nucleus

URI: https://scilib.ai/kg/mathlib#Nucleus.map_himp_apply

English

The map_himp_apply theorem asserts n(x ⇨ ny) = x ⇨ ny, matching the inner nucleus action with implication.

Русский

Теорема map_himp_apply утверждает, что n(x ⇨ ny) = x ⇨ ny.

LaTeX

$$$n(x \Rightarrow n(y)) = x \Rightarrow n(y)$$$

Lean4

theorem map_himp_apply (n : Nucleus X) (x y : X) : n (x ⇨ n y) = x ⇨ n y :=
  le_antisymm (map_himp_le.trans_eq <| by rw [n.idempotent]) n.le_apply

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

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

Разделы

Аффилиация

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