instCardinalInterFilter_cocardinal

English

There is an instance CardinalInterFilter (cocardinal α hreg) c.

Русский

Существует экземпляр CardinalInterFilter для cocardinal α hreg с границей c.

LaTeX

$$CardinalInterFilter (cocardinal α hreg) c$$

Lean4

instance instCardinalInterFilter_cocardinal : CardinalInterFilter (cocardinal (α := α) hreg) c where
  cardinal_sInter_mem S hS
    hSs := by
    rw [mem_cocardinal, Set.compl_sInter]
    apply lt_of_le_of_lt (mk_sUnion_le _)
    apply mul_lt_of_lt hreg.aleph0_le (lt_of_le_of_lt mk_image_le hS)
    apply iSup_lt_of_isRegular hreg <| lt_of_le_of_lt mk_image_le hS
    aesop

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