CountableCover

Statistics

Metric	Count
Definitions	0
Theorems `mk_le_of_countable_eventually_mem`, `mk_of_countable_eventually_mem`, `mk_subtype_le_of_countable_eventually_mem`, `mk_subtype_le_of_countable_eventually_mem_aux`	4
Total	4

Name	Kind	Assumes	Proves	Validates	Depends On
`mk_le_of_countable_eventually_mem` 📖	—	`Filter.Eventually` `Set` `Set.instMembership` `Cardinal` `instLE` `Set.Elem`	—	—	`mk_univ` `mk_subtype_le_of_countable_eventually_mem`
`mk_of_countable_eventually_mem` 📖	—	`Filter.Eventually` `Set` `Set.instMembership` `Set.Elem`	—	—	`le_antisymm` `mk_le_of_countable_eventually_mem` `Eq.le` `Filter.nonempty_of_neBot` `mk_set_le`
`mk_subtype_le_of_countable_eventually_mem` 📖	—	`Filter.Eventually` `Set` `Set.instMembership` `Cardinal` `instLE` `Set.Elem`	—	—	`Filter.map_neBot` `mk_subtype_le_of_countable_eventually_mem_aux` `instCountableULift` `mk_preimage_down`
`mk_subtype_le_of_countable_eventually_mem_aux` 📖	—	`Filter.Eventually` `Set` `Set.instMembership` `Cardinal` `instLE` `Set.Elem`	—	—	`lt_or_ge` `lt_aleph0` `mk_le_iff_forall_finset_subset_card_le` `Finset.eventually_all` `Filter.Eventually.exists` `lt_aleph0_iff_fintype` `LE.le.trans_lt` `Finset.card_le_card` `Set.toFinset_card` `mk_fintype` `LE.le.trans` `Nat.cast_le` `addLeftMono` `IsOrderedRing.toZeroLEOneClass` `isOrderedRing` `instCharZero` `Set.mem_iUnion_of_mem` `mk_le_mk_of_subset` `sum_le_sum` `sum_const` `lift_id` `le_imp_le_of_le_of_le` `mul_le_mul_left` `covariant_swap_mul_of_covariant_mul` `CanonicallyOrderedAdd.toMulLeftMono` `canonicallyOrderedAdd` `mk_le_aleph0` `le_refl` `aleph0_mul_eq`

---