comap_snd_neBot

Mathlib.Order.Filter.Map

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

← MathLib Explorer

English

Duplicate instance for nontrivial comap along Prod.snd.

Русский

Дубликат экземпляра для нетривиального comap вдоль Prod.snd.

LaTeX

$$[Nonempty α] {f} : (f.comap Prod.snd).NeBot$$

Lean4

@[instance]
theorem comap_snd_neBot [Nonempty α] {f : Filter β} [NeBot f] : (f.comap (Prod.snd : α × β → β)).NeBot :=
  comap_snd_neBot_iff.2 ⟨‹_›, ‹_›⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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