Order

Statistics

Metric	Count
Definitions	0
Theorems `eventually_forall_le`, `eventually_forall_lt`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`eventually_forall_le` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `TendstoUniformlyOn` `Preorder.toLE`	`Filter.Eventually`	—	`Filter.mp_mem` `eventually_forall_lt` `Filter.univ_mem'` `LT.lt.le`
`eventually_forall_lt` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `TendstoUniformlyOn` `Preorder.toLE`	`Filter.Eventually`	—	`Filter.eventually_iff_exists_mem` `uniformity_eq_comap_neg_add_nhds_zero` `IsUniformAddGroup.isLeftUniformAddGroup` `IsOpen.mem_nhds` `isOpen_gt'` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `add_zero` `Filter.mp_mem` `Filter.eventually_prod_principal_iff` `Filter.univ_mem'` `add_neg_cancel_left` `add_lt_add_of_le_of_lt`

---