Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-04 19:43 19e7b1f5

View on Github →

feat(analysis/topology): Bounded continuous functions (#464)

Estimated changes

Modified algebra/group.lean

added theorem neg_sub_neg

Modified analysis/metric_space.lean

added theorem bounded.subset

added def bounded

added theorem bounded_bUnion

added theorem bounded_ball

added theorem bounded_closed_ball

added theorem bounded_empty

added theorem bounded_iff_mem_bounded

added theorem bounded_iff_subset_ball

added theorem bounded_of_compact

added theorem bounded_of_compact_space

added theorem bounded_of_finite

added theorem bounded_range_iff

added theorem bounded_singleton

added theorem bounded_union

added theorem cauchy_seq_bdd

added theorem cauchy_seq_iff_le_tendsto_0

added theorem closed_ball_subset_closed_ball

added theorem compact_iff_closed_bounded

added theorem dist_triangle4

added theorem dist_triangle4_left

added theorem dist_triangle4_right

added theorem mem_of_closed'

modified theorem tendsto_at_top_metric

added theorem totally_bounded_of_finite_discretization

Modified analysis/normed_space.lean

added def normed_group.of_add_dist'

added def normed_group.of_add_dist

Created analysis/topology/bounded_continuous_function.lean

added theorem bounded_continuous_function.abs_diff_coe_le_dist

added theorem bounded_continuous_function.arzela_ascoli

added theorem bounded_continuous_function.arzela_ascoli₁

added theorem bounded_continuous_function.arzela_ascoli₂

added theorem bounded_continuous_function.bounded_range

added def bounded_continuous_function.cod_restrict

added theorem bounded_continuous_function.coe_add

added theorem bounded_continuous_function.coe_diff

added theorem bounded_continuous_function.coe_le_coe_add_dist

added theorem bounded_continuous_function.coe_neg

added theorem bounded_continuous_function.coe_zero

added def bounded_continuous_function.comp

added def bounded_continuous_function.const

added theorem bounded_continuous_function.continuous_comp

added theorem bounded_continuous_function.continuous_eval

added theorem bounded_continuous_function.continuous_evalf

added theorem bounded_continuous_function.continuous_evalx

added theorem bounded_continuous_function.dist_coe_le_dist

added theorem bounded_continuous_function.dist_eq

added theorem bounded_continuous_function.dist_le

added theorem bounded_continuous_function.dist_set_exists

added theorem bounded_continuous_function.dist_zero_of_empty

added theorem bounded_continuous_function.equicontinuous_of_continuity_modulus

added theorem bounded_continuous_function.ext

added theorem bounded_continuous_function.forall_coe_zero_iff_zero

added def bounded_continuous_function.mk_of_compact

added def bounded_continuous_function.mk_of_discrete

added theorem bounded_continuous_function.norm_coe_le_norm

added theorem bounded_continuous_function.norm_def

added theorem bounded_continuous_function.norm_le

added def bounded_continuous_function

added theorem continuous_of_lipschitz

added theorem continuous_of_locally_uniform_limit_of_continuous

added theorem continuous_of_uniform_limit_of_continuous

Modified analysis/topology/continuity.lean

added theorem compact_iff_compact_space

added theorem continuous_of_discrete_topology

Modified analysis/topology/uniform_space.lean

added theorem totally_bounded_empty

Modified data/real/ennreal.lean

added theorem ennreal.coe_nonneg

added theorem ennreal.coe_pos

added theorem ennreal.lt_iff_exists_rat_btwn

added theorem ennreal.lt_iff_exists_real_btwn

Modified data/real/nnreal.lean

added theorem nnreal.of_real_add

deleted theorem nnreal.of_real_add_of_real

modified theorem nnreal.of_real_eq_zero

added theorem nnreal.of_real_lt_of_real_iff'

modified theorem nnreal.of_real_lt_of_real_iff

modified theorem nnreal.of_real_of_nonpos

added theorem nnreal.of_real_pos

deleted theorem nnreal.zero_lt_of_real

Modified data/set/basic.lean

added theorem set.range_const_subset

Modified data/set/finite.lean

added theorem set.finite.of_fintype