cardinalInter_ofCardinalUnion

Mathlib.Order.Filter.CardinalInter

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

← MathLib Explorer

English

Instance giving CardinalInterFilter for map f l when l has CardinalInterFilter c.

Русский

Инстанс для CardinalInterFilter фильтра map f l, если l имеет CardinalInterFilter c.

LaTeX

$$$CardinalInterFilter(\\mathrm{map}(f, l), c)$$$

Lean4

instance cardinalInter_ofCardinalUnion (l : Set (Set α)) (hc : 2 < c) (h₁ h₂) :
    CardinalInterFilter (Filter.ofCardinalUnion l hc h₁ h₂) c :=
  cardinalInter_ofCardinalInter ..

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

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

Разделы

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

Аффилиация

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