Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-04 09:49 14d206b3

View on Github →

feat(order/filter/interval): define class filter.is_interval_generated (#3663)

Estimated changes

Modified src/data/set/finite.lean

added theorem set.exists_finite_iff_finset

Modified src/order/filter/bases.lean

added theorem filter.has_basis_infi_principal_finite

Created src/order/filter/interval.lean

added theorem filter.has_basis.is_interval_generated

added theorem filter.has_ord_connected_basis

added theorem filter.is_interval_generated_principal_iff

added theorem filter.tendsto.Icc

added theorem filter.tendsto.Ico

added theorem filter.tendsto.Ioc

added theorem filter.tendsto.Ioo

added theorem filter.tendsto.Ixx

added theorem filter.tendsto_Ixx_same_filter

added theorem set.ord_connected.is_interval_generated_inf_principal

Modified src/topology/algebra/ordered.lean