of_map₂_left

Mathlib.Order.Filter.NAry

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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