of_map₂_right

Mathlib.Order.Filter.NAry

URI: https://scilib.ai/kg/mathlib#Filter.NeBot.of_map₂_right

English

If (map₂ m f g).NeBot then g.NeBot.

Русский

Если (map₂ m f g).NeBot, то g.NeBot.

LaTeX

$$$ (map_2 m f g).\mathrm{NeBot} \Rightarrow g.\mathrm{NeBot} $$$

Lean4

theorem of_map₂_right (h : (map₂ m f g).NeBot) : g.NeBot :=
  (map₂_neBot_iff.1 h).2

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

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

Разделы

Аффилиация

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