coprod_neBot_left

Mathlib.Order.Filter.Prod

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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