theorem Filter.cofinite_hasBasis_Ioi {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [OrderBot α] : cofinite.HasBasis (fun (x : α) => True) fun (x : α) => Set.Ioi x

theorem Filter.cofinite_hasBasis_Ici {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [OrderBot α] [SuccOrder α] [NoMaxOrder α] : cofinite.HasBasis (fun (x : α) => True) fun (x : α) => Set.Ici x

Note(csonne): According to a TODO in Mathlib.Order.Interval.Finset.Defs, Assuming SuccOrder α should not be necessary as an instance should follow from [LocallyFiniteOrder α] [OrderBot α]. This has not been implemented in mathlib however.

theorem Filter.cofinite_eq_atTop {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [OrderBot α] [SuccOrder α] [NoMaxOrder α] : cofinite = atTop