coprod_neBot_right

Mathlib.Order.Filter.Prod

URI: https://scilib.ai/kg/mathlib#Filter.coprod_neBot_right

English

If g is nonempty and α is nonempty, then (f.coprod g).NeBot.

Русский

Если g непусто и α непусто, то (f.coprod g) не пустой.

LaTeX

$$$ [\text{NeBot } g] [\text{Nonempty } \alpha] : (f.coprod g).NeBot $$$

Lean4

@[instance]
theorem coprod_neBot_right [NeBot g] [Nonempty α] : (f.coprod g).NeBot :=
  coprod_neBot_iff.2 (Or.inr ⟨‹_›, ‹_›⟩)

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

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

Разделы

Аффилиация

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