theorem Function.LeftInverse.isOpenMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {g : β → α} (hfg : LeftInverse g f) (hf : IsOpen (Set.range f)) (hg : ContinuousOn g (Set.range f)) : IsOpenMap f

theorem Filter.Eventually.closed_neighborhood {α : Type u_1} [TopologicalSpace α] [NormalSpace α] {C : Set α} {P : α → Prop} (hP : ∀ᶠ (x : α) in nhdsSet C, P x) (hC : IsClosed C) : ∃ C' ∈ nhdsSet C, IsClosed C' ∧ ∀ᶠ (x : α) in nhdsSet C', P x

theorem support_norm {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] (f : α → E) : (Function.support fun (a : α) => ‖f a‖) = Function.support f

theorem hasCompactMulSupport_of_subset {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [T2Space α] [One β] {f : α → β} {K : Set α} (hK : IsCompact K) (hf : Function.mulSupport f ⊆ K) : HasCompactMulSupport f

theorem hasCompactSupport_of_subset {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [T2Space α] [Zero β] {f : α → β} {K : Set α} (hK : IsCompact K) (hf : Function.support f ⊆ K) : HasCompactSupport f

theorem periodic_const {α : Type u_1} {β : Type u_2} [Add α] {a : α} {b : β} : Function.Periodic (fun (x : α) => b) a

The standard ℤ action on ℝ is properly discontinuous

TODO: use that in ToMathlib.Algebra.Periodic?

@[implicit_reducible]

instance instVAddIntReal_sphereEversion : VAdd ℤ ℝ

Equations

• instVAddIntReal_sphereEversion = { vadd := fun (n : ℤ) (x : ℝ) => ↑n + x }

instance instProperlyDiscontinuousVAddIntReal_sphereEversion : ProperlyDiscontinuousVAdd ℤ ℝ

theorem Ioo_floor_mem_nhds {x : ℝ} (h : x ∉ Set.range Int.cast) : Set.Ioo (↑⌊x⌋) (↑⌊x⌋ + 1) ∈ nhds x

theorem loc_constant_floor {x : ℝ} (h : x ∉ Set.range Int.cast) : Int.floor =ᶠ[nhds x] fun (x_1 : ℝ) => ⌊x⌋

theorem fract_eventuallyEq {x : ℝ} (h : Int.fract x ≠ 0) : Int.fract =ᶠ[nhds x] fun (x' : ℝ) => x' - ↑⌊x⌋

theorem Ioo_inter_Iio {α : Type u_1} [LinearOrder α] {a b c : α} : Set.Ioo a b ∩ Set.Iio c = Set.Ioo a (min b c)

theorem fract_lt {x y : ℝ} {n : ℤ} (h1 : ↑n ≤ x) (h2 : x < ↑n + y) : Int.fract x < y

theorem one_sub_lt_fract {x y : ℝ} {n : ℤ} (hy : y ≤ 1) (h1 : ↑n - y < x) (h2 : x < ↑n) : 1 - y < Int.fract x

theorem IsOpen.preimage_fract' {s : Set ℝ} (hs : IsOpen s) (h2s : 0 ∈ s → s ∈ nhdsWithin 1 (Set.Iio 1)) : IsOpen (Int.fract ⁻¹' s)

theorem IsOpen.preimage_fract {s : Set ℝ} (hs : IsOpen s) (h2s : 0 ∈ s → 1 ∈ s) : IsOpen (Int.fract ⁻¹' s)

theorem IsClosed.preimage_fract {s : Set ℝ} (hs : IsClosed s) (h2s : sᶜ ∉ nhdsWithin 1 (Set.Iio 1) → 0 ∈ s) : IsClosed (Int.fract ⁻¹' s)

theorem fract_preimage_mem_nhds {s : Set ℝ} {x : ℝ} (h1 : s ∈ nhds (Int.fract x)) (h2 : Int.fract x = 0 → s ∈ nhds 1) : Int.fract ⁻¹' s ∈ nhds x

theorem isOpen_slice_of_isOpen_over {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {Ω : Set (α × β)} {x₀ : α} (hΩ_op : ∃ U ∈ nhds x₀, IsOpen (Ω ∩ Prod.fst ⁻¹' U)) : IsOpen (Prod.mk x₀ ⁻¹' Ω)

def projI {α : Type u_1} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] : α → α

If α is a LinearOrderedSemiring, then projI : α → α projection of α onto the unit interval [0, 1].

Equations

• projI x = ↑(Set.projIcc 0 1 ⋯ x)

theorem projI_def {α : Type u_1} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] {x : α} : projI x = max 0 (min 1 x)

theorem projIcc_eq_projI {α : Type u_1} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] {x : α} : ↑(Set.projIcc 0 1 ⋯ x) = projI x

theorem projI_of_le_zero {α : Type u_1} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] {x : α} (hx : x ≤ 0) : projI x = 0

@[simp]

theorem projI_zero {α : Type u_1} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] : projI 0 = 0

theorem projI_of_one_le {α : Type u_1} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] {x : α} (hx : 1 ≤ x) : projI x = 1

@[simp]

theorem projI_one {α : Type u_1} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] : projI 1 = 1

@[simp]

theorem projI_eq_zero {α : Type u_1} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] {x : α} : projI x = 0 ↔ x ≤ 0

@[simp]

theorem projI_eq_one {α : Type u_1} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] {x : α} : projI x = 1 ↔ 1 ≤ x

theorem projI_mem_Icc {α : Type u_1} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] {x : α} : projI x ∈ Set.Icc 0 1

theorem projI_eq_self {α : Type u_1} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] {x : α} : projI x = x ↔ x ∈ Set.Icc 0 1

@[simp]

theorem projI_projI {α : Type u_1} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] {x : α} : projI (projI x) = projI x

@[simp]

theorem projIcc_projI {α : Type u_1} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] {x : α} : Set.projIcc 0 1 ⋯ (projI x) = Set.projIcc 0 1 ⋯ x

@[simp]

theorem range_projI : Set.range projI = Set.Icc 0 1

theorem monotone_projI {α : Type u_1} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] : Monotone projI

theorem strictMonoOn_projI {α : Type u_1} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] : StrictMonoOn projI (Set.Icc 0 1)

theorem projI_le_max {α : Type u_1} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] {x : α} : projI x ≤ max 0 x

theorem min_le_projI {α : Type u_1} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] {x : α} : min 1 x ≤ projI x

theorem projI_le_iff {α : Type u_1} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] {x c : α} : projI x ≤ c ↔ 0 ≤ c ∧ (1 ≤ c ∨ x ≤ c)

@[simp]

theorem projI_eq_min {α : Type u_1} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] {x : α} : projI x = min 1 x ↔ 0 ≤ x

theorem min_projI {α : Type u_1} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] {x c : α} (h2 : 0 ≤ c) : min c (projI x) = projI (min c x)

theorem continuous_projI {α : Type u_1} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [TopologicalSpace α] [OrderTopology α] : Continuous projI

theorem projI_mapsto {α : Type u_1} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] {s : Set α} (h0s : 0 ∈ s) (h1s : 1 ∈ s) : Set.MapsTo projI s s

theorem truncate_projI_right {X : Type u_3} [TopologicalSpace X] {a b : X} (γ : Path a b) (t₀ t₁ : ℝ) (s : ↑unitInterval) : (γ.truncate t₀ (projI t₁)) s = (γ.truncate t₀ t₁) s

theorem decode₂_locallyFinite {α : Type u_1} [TopologicalSpace α] {ι : Type u_1} [Encodable ι] {s : ι → Set α} (hs : LocallyFinite s) : LocallyFinite fun (i : ℕ) => (s <$> Encodable.decode₂ ι i).getD ∅

Given a locally finite sequence of sets indexed by an encodable type, we can naturally reindex this sequence to get a sequence indexed by ℕ (by adding some ∅ values). This new sequence is still locally finite.

theorem exists_locallyFinite_subcover_of_locally {X : Type u_4} [EMetricSpace X] [LocallyCompactSpace X] [SecondCountableTopology X] {C : Set X} (hC : IsClosed C) {P : Set X → Prop} (hP : Antitone P) (h0 : P ∅) (hX : ∀ x ∈ C, ∃ V ∈ nhds x, P V) : ∃ (K : ℕ → Set X) (W : ℕ → Set X), (∀ (n : ℕ), IsCompact (K n)) ∧ (∀ (n : ℕ), IsOpen (W n)) ∧ (∀ (n : ℕ), P (W n)) ∧ (∀ (n : ℕ), K n ⊆ W n) ∧ LocallyFinite W ∧ C ⊆ ⋃ (n : ℕ), K n

theorem IsCompact.eventually_forall_mem {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {x₀ : α} {K : Set β} (hK : IsCompact K) {f : α → β → γ} (hf : Continuous ↿f) {U : Set γ} (hU : ∀ y ∈ K, U ∈ nhds (f x₀ y)) : ∀ᶠ (x : α) in nhds x₀, ∀ y ∈ K, f x y ∈ U

theorem Continuous.infDist {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [PseudoMetricSpace β] {s : Set β} {f : α → β} (hf : Continuous f) : Continuous fun (x : α) => Metric.infDist (f x) s

theorem isPreconnected_ball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (x : E) (r : ℝ) : IsPreconnected (Metric.ball x r)

theorem isConnected_ball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {r : ℝ} : IsConnected (Metric.ball x r) ↔ 0 < r

theorem TopologicalSpace.cover_nat_nhdsWithin {α : Type u_1} [TopologicalSpace α] [SecondCountableTopology α] {f : α → Set α} {s : Set α} (hf : ∀ x ∈ s, f x ∈ nhdsWithin x s) (hs : s.Nonempty) : ∃ (x : ℕ → α), Set.range x ⊆ s ∧ s ⊆ ⋃ (n : ℕ), f (x n)

theorem TopologicalSpace.cover_nat_nhdsWithin' {α : Type u_1} [TopologicalSpace α] [SecondCountableTopology α] {s : Set α} {f : (x : α) → x ∈ s → Set α} (hf : ∀ (x : α) (hx : x ∈ s), f x hx ∈ nhdsWithin x s) (hs : s.Nonempty) : ∃ (x : ℕ → α) (hx : Set.range x ⊆ s), s ⊆ ⋃ (n : ℕ), f (x n) ⋯

A version of TopologicalSpace.cover_nat_nhdsWithin where f is only defined on s.

theorem Set.Subtype.image_coe_eq_iff_eq_univ {α : Type u_1} {s : Set α} {t : Set ↑s} : Subtype.val '' t = s ↔ t = univ

theorem Set.Subtype.preimage_coe_eq_univ {α : Type u_1} {s t : Set α} : Subtype.val ⁻¹' t = univ ↔ s ⊆ t

theorem precise_refinement_set' {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {s : Set X} [ParacompactSpace ↑s] (hs : IsOpen s) (u : ι → Set X) (uo : ∀ (i : ι), IsOpen (u i)) (us : s ⊆ ⋃ (i : ι), u i) : ∃ (v : ι → Set X), (∀ (i : ι), IsOpen (v i)) ∧ s ⊆ ⋃ (i : ι), v i ∧ (LocallyFinite fun (i : ι) => Subtype.val ⁻¹' v i) ∧ (∀ (i : ι), v i ⊆ s) ∧ ∀ (i : ι), v i ⊆ u i

When s : Set X is open and paracompact, we can find a precise refinement on s. Note that in this case we only get the locally finiteness condition on s, which is weaker than the local finiteness condition on all of X (the collection might not be locally finite on the boundary of s).

theorem point_finite_of_locallyFinite_coe_preimage {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {s : Set X} {f : ι → Set X} (hf : LocallyFinite fun (i : ι) => Subtype.val ⁻¹' f i) (hfs : ∀ (i : ι), f i ⊆ s) {x : X} : {i : ι | x ∈ f i}.Finite

theorem exists_subset_iUnion_interior_of_isOpen {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {u : ι → Set X} {s : Set X} [NormalSpace ↑s] (hs : IsOpen s) (uo : ∀ (i : ι), IsOpen (u i)) (uc : ∀ (i : ι), IsCompact (closure (u i))) (us : ∀ (i : ι), closure (u i) ⊆ s) (uf : ∀ x ∈ s, {i : ι | x ∈ u i}.Finite) (uU : s ⊆ ⋃ (i : ι), u i) : ∃ (v : ι → Set X), s ⊆ ⋃ (i : ι), interior (v i) ∧ (∀ (i : ι), IsCompact (v i)) ∧ ∀ (i : ι), v i ⊆ u i

theorem Filter.EventuallyEq.slice {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] {f g : α × β → γ} {a : α} {b : β} (h : f =ᶠ[nhds (a, b)] g) : (fun (y : β) => f (a, y)) =ᶠ[nhds b] fun (y : β) => g (a, y)

theorem exists_compact_between' {α : Type u_1} [TopologicalSpace α] [LocallyCompactSpace α] {K U : Set α} (hK : IsCompact K) (hU : IsOpen U) (h_KU : K ⊆ U) : ∃ (L : Set α), IsCompact L ∧ L ∈ nhdsSet K ∧ L ⊆ U