Loogle!

Result

Found 189 declarations mentioning IsPreconnected.

• IsPreconnected 📋 Mathlib.Topology.Connected.Basic
  {α : Type u} [TopologicalSpace α] (s : Set α) : Prop
• isPreconnected_connectedComponent 📋 Mathlib.Topology.Connected.Basic
  {α : Type u} [TopologicalSpace α] {x : α} : IsPreconnected (connectedComponent x)
• isPreconnected_empty 📋 Mathlib.Topology.Connected.Basic
  {α : Type u} [TopologicalSpace α] : IsPreconnected ∅
• PreconnectedSpace.isPreconnected_univ 📋 Mathlib.Topology.Connected.Basic
  {α : Type u} {inst✝ : TopologicalSpace α} [self : PreconnectedSpace α] : IsPreconnected Set.univ
• PreconnectedSpace.mk 📋 Mathlib.Topology.Connected.Basic
  {α : Type u} [TopologicalSpace α] (isPreconnected_univ : IsPreconnected Set.univ) : PreconnectedSpace α
• preconnectedSpace_iff_univ 📋 Mathlib.Topology.Connected.Basic
  {α : Type u} [TopologicalSpace α] : PreconnectedSpace α ↔ IsPreconnected Set.univ
• Set.Subsingleton.isPreconnected 📋 Mathlib.Topology.Connected.Basic
  {α : Type u} [TopologicalSpace α] {s : Set α} (hs : s.Subsingleton) : IsPreconnected s
• IsConnected.isPreconnected 📋 Mathlib.Topology.Connected.Basic
  {α : Type u} [TopologicalSpace α] {s : Set α} (h : IsConnected s) : IsPreconnected s
• IsPreirreducible.isPreconnected 📋 Mathlib.Topology.Connected.Basic
  {α : Type u} [TopologicalSpace α] {s : Set α} (H : IsPreirreducible s) : IsPreconnected s
• isPreconnected_connectedComponentIn 📋 Mathlib.Topology.Connected.Basic
  {α : Type u} [TopologicalSpace α] {x : α} {F : Set α} : IsPreconnected (connectedComponentIn F x)
• isPreconnected_singleton 📋 Mathlib.Topology.Connected.Basic
  {α : Type u} [TopologicalSpace α] {x : α} : IsPreconnected {x}
• IsPreconnected.closure 📋 Mathlib.Topology.Connected.Basic
  {α : Type u} [TopologicalSpace α] {s : Set α} (H : IsPreconnected s) : IsPreconnected (closure s)
• isPreconnected_range 📋 Mathlib.Topology.Connected.Basic
  {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [PreconnectedSpace α] {f : α → β} (h : Continuous f) : IsPreconnected (Set.range f)
• Subtype.preconnectedSpace 📋 Mathlib.Topology.Connected.Basic
  {α : Type u} [TopologicalSpace α] {s : Set α} (h : IsPreconnected s) : PreconnectedSpace ↑s
• isPreconnected_iff_preconnectedSpace 📋 Mathlib.Topology.Connected.Basic
  {α : Type u} [TopologicalSpace α] {s : Set α} : IsPreconnected s ↔ PreconnectedSpace ↑s
• IsPreconnected.connectedComponentIn 📋 Mathlib.Topology.Connected.Basic
  {α : Type u} [TopologicalSpace α] {x : α} {F : Set α} (h : IsPreconnected F) (hx : x ∈ F) : connectedComponentIn F x = F
• IsPreconnected.subset_connectedComponent 📋 Mathlib.Topology.Connected.Basic
  {α : Type u} [TopologicalSpace α] {x : α} {s : Set α} (H1 : IsPreconnected s) (H2 : x ∈ s) : s ⊆ connectedComponent x
• IsPreconnected.image 📋 Mathlib.Topology.Connected.Basic
  {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} (H : IsPreconnected s) (f : α → β) (hf : ContinuousOn f s) : IsPreconnected (f '' s)
• Topology.IsInducing.isPreconnected_image 📋 Mathlib.Topology.Connected.Basic
  {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {f : α → β} (hf : Topology.IsInducing f) : IsPreconnected (f '' s) ↔ IsPreconnected s
• isPreconnected_iUnion 📋 Mathlib.Topology.Connected.Basic
  {α : Type u} [TopologicalSpace α] {ι : Sort u_3} {s : ι → Set α} (h₁ : (⋂ i, s i).Nonempty) (h₂ : ∀ (i : ι), IsPreconnected (s i)) : IsPreconnected (⋃ i, s i)
• IsPreconnected.subset_closure 📋 Mathlib.Topology.Connected.Basic
  {α : Type u} [TopologicalSpace α] {s t : Set α} (H : IsPreconnected s) (Kst : s ⊆ t) (Ktcs : t ⊆ closure s) : IsPreconnected t
• isPreconnected_univ_pi 📋 Mathlib.Topology.Connected.Basic
  {ι : Type u_1} {X : ι → Type u_2} [(i : ι) → TopologicalSpace (X i)] {s : (i : ι) → Set (X i)} (hs : ∀ (i : ι), IsPreconnected (s i)) : IsPreconnected (Set.univ.pi s)
• IsPreconnected.union' 📋 Mathlib.Topology.Connected.Basic
  {α : Type u} [TopologicalSpace α] {s t : Set α} (H : (s ∩ t).Nonempty) (hs : IsPreconnected s) (ht : IsPreconnected t) : IsPreconnected (s ∪ t)
• IsPreconnected.subset_connectedComponentIn 📋 Mathlib.Topology.Connected.Basic
  {α : Type u} [TopologicalSpace α] {s : Set α} {x : α} {F : Set α} (hs : IsPreconnected s) (hxs : x ∈ s) (hsF : s ⊆ F) : s ⊆ connectedComponentIn F x
• IsPreconnected.iUnion_of_reflTransGen 📋 Mathlib.Topology.Connected.Basic
  {α : Type u} [TopologicalSpace α] {ι : Type u_3} {s : ι → Set α} (H : ∀ (i : ι), IsPreconnected (s i)) (K : ∀ (i j : ι), Relation.ReflTransGen (fun i j => (s i ∩ s j).Nonempty) i j) : IsPreconnected (⋃ n, s n)
• IsPreconnected.prod 📋 Mathlib.Topology.Connected.Basic
  {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {t : Set β} (hs : IsPreconnected s) (ht : IsPreconnected t) : IsPreconnected (s ×ˢ t)
• IsPreconnected.preimage_of_isClosedMap 📋 Mathlib.Topology.Connected.Basic
  {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {s : Set β} (hs : IsPreconnected s) {f : α → β} (hinj : Function.Injective f) (hf : IsClosedMap f) (hsf : s ⊆ Set.range f) : IsPreconnected (f ⁻¹' s)
• IsPreconnected.preimage_of_isOpenMap 📋 Mathlib.Topology.Connected.Basic
  {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set β} (hs : IsPreconnected s) (hinj : Function.Injective f) (hf : IsOpenMap f) (hsf : s ⊆ Set.range f) : IsPreconnected (f ⁻¹' s)
• IsPreconnected.union 📋 Mathlib.Topology.Connected.Basic
  {α : Type u} [TopologicalSpace α] (x : α) {s t : Set α} (H1 : x ∈ s) (H2 : x ∈ t) (H3 : IsPreconnected s) (H4 : IsPreconnected t) : IsPreconnected (s ∪ t)
• IsPreconnected.sUnion_directed 📋 Mathlib.Topology.Connected.Basic
  {α : Type u} [TopologicalSpace α] {S : Set (Set α)} (K : DirectedOn (fun x1 x2 => x1 ⊆ x2) S) (H : ∀ s ∈ S, IsPreconnected s) : IsPreconnected (⋃₀ S)
• IsPreconnected.subset_of_closure_inter_subset 📋 Mathlib.Topology.Connected.Basic
  {α : Type u} [TopologicalSpace α] {s u : Set α} (hs : IsPreconnected s) (hu : IsOpen u) (h'u : (s ∩ u).Nonempty) (h : closure u ∩ s ⊆ u) : s ⊆ u
• IsPreconnected.transGen_of_iUnion 📋 Mathlib.Topology.Connected.Basic
  {α : Type u} [TopologicalSpace α] {ι : Type u_3} {s : ι → Set α} (hs : IsPreconnected (⋃ n, s n)) (hs' : ∀ (i : ι), IsOpen (s i)) (i j : ι) (hi : (s i).Nonempty) (hj : (s j).Nonempty) : Relation.TransGen (fun a b => (s a ∩ s b).Nonempty) i j
• isPreconnected_sUnion 📋 Mathlib.Topology.Connected.Basic
  {α : Type u} [TopologicalSpace α] (x : α) (c : Set (Set α)) (H1 : ∀ s ∈ c, x ∈ s) (H2 : ∀ s ∈ c, IsPreconnected s) : IsPreconnected (⋃₀ c)
• isPreconnected_of_forall 📋 Mathlib.Topology.Connected.Basic
  {α : Type u} [TopologicalSpace α] {s : Set α} (x : α) (H : ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t) : IsPreconnected s
• isPreconnected_of_forall_pair 📋 Mathlib.Topology.Connected.Basic
  {α : Type u} [TopologicalSpace α] {s : Set α} (H : ∀ x ∈ s, ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t) : IsPreconnected s
• isPreconnected_closed_iff 📋 Mathlib.Topology.Connected.Basic
  {α : Type u} [TopologicalSpace α] {s : Set α} : IsPreconnected s ↔ ∀ (t t' : Set α), IsClosed t → IsClosed t' → s ⊆ t ∪ t' → (s ∩ t).Nonempty → (s ∩ t').Nonempty → (s ∩ (t ∩ t')).Nonempty
• IsPreconnected.iUnion_of_chain 📋 Mathlib.Topology.Connected.Basic
  {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder β] [SuccOrder β] [IsSuccArchimedean β] {s : β → Set α} (H : ∀ (n : β), IsPreconnected (s n)) (K : ∀ (n : β), (s n ∩ s (Order.succ n)).Nonempty) : IsPreconnected (⋃ n, s n)
• IsPreconnected.mapsTo_Ioi_or_Iio 📋 Mathlib.Topology.Connected.Basic
  {α : Type u} {β : Type v} [TopologicalSpace α] {s : Set α} [LinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {b : β} (hs : IsPreconnected s) (hf : ContinuousOn f s) (hfb : ∀ x ∈ s, f x ≠ b) : Set.MapsTo f s (Set.Ioi b) ∨ Set.MapsTo f s (Set.Iio b)
• IsPreconnected.subset_or_subset 📋 Mathlib.Topology.Connected.Basic
  {α : Type u} [TopologicalSpace α] {s u v : Set α} (hu : IsOpen u) (hv : IsOpen v) (huv : Disjoint u v) (hsuv : s ⊆ u ∪ v) (hs : IsPreconnected s) : s ⊆ u ∨ s ⊆ v
• IsPreconnected.subset_left_of_subset_union 📋 Mathlib.Topology.Connected.Basic
  {α : Type u} [TopologicalSpace α] {s u v : Set α} (hu : IsOpen u) (hv : IsOpen v) (huv : Disjoint u v) (hsuv : s ⊆ u ∪ v) (hsu : (s ∩ u).Nonempty) (hs : IsPreconnected s) : s ⊆ u
• IsPreconnected.subset_right_of_subset_union 📋 Mathlib.Topology.Connected.Basic
  {α : Type u} [TopologicalSpace α] {s u v : Set α} (hu : IsOpen u) (hv : IsOpen v) (huv : Disjoint u v) (hsuv : s ⊆ u ∪ v) (hsv : (s ∩ v).Nonempty) (hs : IsPreconnected s) : s ⊆ v
• IsPreconnected.biUnion_of_reflTransGen 📋 Mathlib.Topology.Connected.Basic
  {α : Type u} [TopologicalSpace α] {ι : Type u_3} {t : Set ι} {s : ι → Set α} (H : ∀ i ∈ t, IsPreconnected (s i)) (K : ∀ i ∈ t, ∀ j ∈ t, Relation.ReflTransGen (fun i j => (s i ∩ s j).Nonempty ∧ i ∈ t) i j) : IsPreconnected (⋃ n ∈ t, s n)
• IsPreconnected.gt_of_ne 📋 Mathlib.Topology.Connected.Basic
  {α : Type u} {β : Type v} [TopologicalSpace α] {s : Set α} [LinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {b : β} (hs : IsPreconnected s) (hf : ContinuousOn f s) (hfb : ∀ x ∈ s, f x ≠ b) (hfx : ∃ x ∈ s, f x < b) {x : α} (hx : x ∈ s) : f x < b
• IsPreconnected.lt_of_ne 📋 Mathlib.Topology.Connected.Basic
  {α : Type u} {β : Type v} [TopologicalSpace α] {s : Set α} [LinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {b : β} (hs : IsPreconnected s) (hf : ContinuousOn f s) (hfb : ∀ x ∈ s, f x ≠ b) (hfx : ∃ x ∈ s, b < f x) {x : α} (hx : x ∈ s) : b < f x
• IsPreconnected.biUnion_of_chain 📋 Mathlib.Topology.Connected.Basic
  {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder β] [SuccOrder β] [IsSuccArchimedean β] {s : β → Set α} {t : Set β} (ht : t.OrdConnected) (H : ∀ n ∈ t, IsPreconnected (s n)) (K : ∀ n ∈ t, Order.succ n ∈ t → (s n ∩ s (Order.succ n)).Nonempty) : IsPreconnected (⋃ n ∈ t, s n)
• IsPreconnected.subset_isClopen 📋 Mathlib.Topology.Connected.Clopen
  {α : Type u} [TopologicalSpace α] {s t : Set α} (hs : IsPreconnected s) (ht : IsClopen t) (hne : (s ∩ t).Nonempty) : s ⊆ t
• isPreconnected_of_forall_constant 📋 Mathlib.Topology.Connected.Clopen
  {α : Type u} [TopologicalSpace α] {s : Set α} (hs : ∀ (f : α → Bool), ContinuousOn f s → ∀ x ∈ s, ∀ y ∈ s, f x = f y) : IsPreconnected s
• disjoint_or_subset_of_isClopen 📋 Mathlib.Topology.Connected.Clopen
  {α : Type u} [TopologicalSpace α] {s t : Set α} (hs : IsPreconnected s) (ht : IsClopen t) : Disjoint s t ∨ s ⊆ t
• Sigma.isPreconnected_iff 📋 Mathlib.Topology.Connected.Clopen
  {ι : Type u_1} {X : ι → Type u_2} [hι : Nonempty ι] [(i : ι) → TopologicalSpace (X i)] {s : Set ((i : ι) × X i)} : IsPreconnected s ↔ ∃ i t, IsPreconnected t ∧ s = Sigma.mk i '' t
• isPreconnected_iff_subset_of_disjoint 📋 Mathlib.Topology.Connected.Clopen
  {α : Type u} [TopologicalSpace α] {s : Set α} : IsPreconnected s ↔ ∀ (u v : Set α), IsOpen u → IsOpen v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
• isPreconnected_iff_subset_of_disjoint_closed 📋 Mathlib.Topology.Connected.Clopen
  {α : Type u} [TopologicalSpace α] {s : Set α} : IsPreconnected s ↔ ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
• Sum.isPreconnected_iff 📋 Mathlib.Topology.Connected.Clopen
  {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {s : Set (α ⊕ β)} : IsPreconnected s ↔ (∃ t, IsPreconnected t ∧ s = Sum.inl '' t) ∨ ∃ t, IsPreconnected t ∧ s = Sum.inr '' t
• IsClopen.isPreconnected_iff 📋 Mathlib.Topology.Connected.Clopen
  {α : Type u} [TopologicalSpace α] {s : Set α} (hs : IsClopen s) : IsPreconnected s ↔ ∀ (a b : Set α), IsClopen a → IsClopen b → a.Nonempty → b.Nonempty → Disjoint a b → s ≠ a ∪ b
• IsPreconnected.induction₂' 📋 Mathlib.Topology.Connected.Clopen
  {α : Type u} [TopologicalSpace α] {s : Set α} (hs : IsPreconnected s) (P : α → α → Prop) (h : ∀ x ∈ s, ∀ᶠ (y : α) in nhdsWithin x s, P x y ∧ P y x) (h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z) {x y : α} (hx : x ∈ s) (hy : y ∈ s) : P x y
• isPreconnected_iff_subset_of_fully_disjoint_closed 📋 Mathlib.Topology.Connected.Clopen
  {α : Type u} [TopologicalSpace α] {s : Set α} (hs : IsClosed s) : IsPreconnected s ↔ ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
• IsClopen.not_isPreconnected_iff 📋 Mathlib.Topology.Connected.Clopen
  {α : Type u} [TopologicalSpace α] {s : Set α} (hs : IsClopen s) : ¬IsPreconnected s ↔ ∃ a b, IsClopen a ∧ IsClopen b ∧ a.Nonempty ∧ b.Nonempty ∧ Disjoint a b ∧ s = a ∪ b
• IsPreconnected.induction₂ 📋 Mathlib.Topology.Connected.Clopen
  {α : Type u} [TopologicalSpace α] {s : Set α} (hs : IsPreconnected s) (P : α → α → Prop) (h : ∀ x ∈ s, ∀ᶠ (y : α) in nhdsWithin x s, P x y) (h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z) (h'' : ∀ (x y : α), x ∈ s → y ∈ s → P x y → P y x) {x y : α} (hx : x ∈ s) (hy : y ∈ s) : P x y
• TopologicalSpace.IsTopologicalBasis.isOpen_isPreconnected 📋 Mathlib.Topology.Connected.LocallyConnected
  {α : Type u} [TopologicalSpace α] [LocallyConnectedSpace α] : TopologicalSpace.IsTopologicalBasis {s | IsOpen s ∧ IsPreconnected s}
• locallyConnectedSpace_iff_isTopologicalBasis_isOpen_isPreconnected 📋 Mathlib.Topology.Connected.LocallyConnected
  {α : Type u} [TopologicalSpace α] : LocallyConnectedSpace α ↔ TopologicalSpace.IsTopologicalBasis {s | IsOpen s ∧ IsPreconnected s}
• locallyConnectedSpace_of_connected_bases 📋 Mathlib.Topology.Connected.LocallyConnected
  {α : Type u} [TopologicalSpace α] {ι : Type u_3} (b : α → ι → Set α) (p : α → ι → Prop) (hbasis : ∀ (x : α), (nhds x).HasBasis (p x) (b x)) (hconnected : ∀ (x : α) (i : ι), p x i → IsPreconnected (b x i)) : LocallyConnectedSpace α
• locallyConnectedSpace_iff_connected_basis 📋 Mathlib.Topology.Connected.LocallyConnected
  {α : Type u} [TopologicalSpace α] : LocallyConnectedSpace α ↔ ∀ (x : α), (nhds x).HasBasis (fun s => s ∈ nhds x ∧ IsPreconnected s) id
• locallyConnectedSpace_iff_connected_subsets 📋 Mathlib.Topology.Connected.LocallyConnected
  {α : Type u} [TopologicalSpace α] : LocallyConnectedSpace α ↔ ∀ (x : α), ∀ U ∈ nhds x, ∃ V ∈ nhds x, IsPreconnected V ∧ V ⊆ U
• IsPreconnected.subsingleton 📋 Mathlib.Topology.Connected.TotallyDisconnected
  {α : Type u} [TopologicalSpace α] [TotallyDisconnectedSpace α] {s : Set α} (h : IsPreconnected s) : s.Subsingleton
• IsPreconnected.isDiscrete_iff_subsingleton 📋 Mathlib.Topology.Connected.TotallyDisconnected
  {α : Type u} [TopologicalSpace α] {S : Set α} (hS : IsPreconnected S) : IsDiscrete S ↔ S.Subsingleton
• IsPreconnected.constant 📋 Mathlib.Topology.Connected.TotallyDisconnected
  {α : Type u} [TopologicalSpace α] {Y : Type u_3} [TopologicalSpace Y] [DiscreteTopology Y] {s : Set α} (hs : IsPreconnected s) {f : α → Y} (hf : ContinuousOn f s) {x y : α} (hx : x ∈ s) (hy : y ∈ s) : f x = f y
• IsPreconnected.constant_of_mapsTo 📋 Mathlib.Topology.Connected.TotallyDisconnected
  {α : Type u} [TopologicalSpace α] {S : Set α} (hS : IsPreconnected S) {β : Type u_3} [TopologicalSpace β] {T : Set β} (hT : IsDiscrete T) {f : α → β} (hc : ContinuousOn f S) (hTm : Set.MapsTo f S T) {x y : α} (hx : x ∈ S) (hy : y ∈ S) : f x = f y
• IsPreconnected.eqOn_const_of_mapsTo 📋 Mathlib.Topology.Connected.TotallyDisconnected
  {α : Type u} [TopologicalSpace α] {S : Set α} (hS : IsPreconnected S) {β : Type u_3} [TopologicalSpace β] {T : Set β} (hT : IsDiscrete T) {f : α → β} (hc : ContinuousOn f S) (hTm : Set.MapsTo f S T) (hne : T.Nonempty) : ∃ y ∈ T, Set.EqOn f (Function.const α y) S
• Homeomorph.isPreconnected_image 📋 Mathlib.Topology.Homeomorph.Lemmas
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} (h : X ≃ₜ Y) : IsPreconnected (⇑h '' s) ↔ IsPreconnected s
• Homeomorph.isPreconnected_preimage 📋 Mathlib.Topology.Homeomorph.Lemmas
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set Y} (h : X ≃ₜ Y) : IsPreconnected (⇑h ⁻¹' s) ↔ IsPreconnected s
• IsPreconnected.eq_one_or_eq_neg_one_of_sq_eq 📋 Mathlib.Topology.Algebra.Field
  {α : Type u_2} {𝕜 : Type u_3} {f : α → 𝕜} {S : Set α} [TopologicalSpace α] [TopologicalSpace 𝕜] [T1Space 𝕜] [Ring 𝕜] [NoZeroDivisors 𝕜] (hS : IsPreconnected S) (hf : ContinuousOn f S) (hsq : Set.EqOn (f ^ 2) 1 S) : Set.EqOn f 1 S ∨ Set.EqOn f (-1) S
• IsPreconnected.eq_of_sq_eq 📋 Mathlib.Topology.Algebra.Field
  {α : Type u_2} {𝕜 : Type u_3} {f g : α → 𝕜} {S : Set α} [TopologicalSpace α] [TopologicalSpace 𝕜] [T1Space 𝕜] [Field 𝕜] [ContinuousInv₀ 𝕜] [ContinuousMul 𝕜] (hS : IsPreconnected S) (hf : ContinuousOn f S) (hg : ContinuousOn g S) (hsq : Set.EqOn (f ^ 2) (g ^ 2) S) (hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0) {y : α} (hy : y ∈ S) (hy' : f y = g y) : Set.EqOn f g S
• IsPreconnected.eq_or_eq_neg_of_sq_eq 📋 Mathlib.Topology.Algebra.Field
  {α : Type u_2} {𝕜 : Type u_3} {f g : α → 𝕜} {S : Set α} [TopologicalSpace α] [TopologicalSpace 𝕜] [T1Space 𝕜] [Field 𝕜] [ContinuousInv₀ 𝕜] [ContinuousMul 𝕜] (hS : IsPreconnected S) (hf : ContinuousOn f S) (hg : ContinuousOn g S) (hsq : Set.EqOn (f ^ 2) (g ^ 2) S) (hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0) : Set.EqOn f g S ∨ Set.EqOn f (-g) S
• IsLocallyConstant.apply_eq_of_isPreconnected 📋 Mathlib.Topology.LocallyConstant.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} (hf : IsLocallyConstant f) {s : Set X} (hs : IsPreconnected s) {x y : X} (hx : x ∈ s) (hy : y ∈ s) : f x = f y
• IsLocallyConstant.of_constant_on_preconnected_clopens 📋 Mathlib.Topology.LocallyConstant.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [LocallyConnectedSpace X] {f : X → Y} (h : ∀ (U : Set X), IsPreconnected U → IsClopen U → ∀ x ∈ U, ∀ y ∈ U, f y = f x) : IsLocallyConstant f
• LocallyConstant.apply_eq_of_isPreconnected 📋 Mathlib.Topology.LocallyConstant.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] (f : LocallyConstant X Y) {s : Set X} (hs : IsPreconnected s) {x y : X} (hx : x ∈ s) (hy : y ∈ s) : f x = f y
• IsPreconnected.ordConnected 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type v} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set α} (h : IsPreconnected s) : s.OrdConnected
• isPreconnected_uIoc 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {a b : α} : IsPreconnected (Set.uIoc a b)
• isPreconnected_uIoo 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {a b : α} : IsPreconnected (Set.uIoo a b)
• isPreconnected_uIcc 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {a b : α} : IsPreconnected (Set.uIcc a b)
• isPreconnected_Ici 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} : IsPreconnected (Set.Ici a)
• isPreconnected_Iic 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} : IsPreconnected (Set.Iic a)
• isPreconnected_Iio 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} : IsPreconnected (Set.Iio a)
• isPreconnected_Ioi 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} : IsPreconnected (Set.Ioi a)
• isPreconnected_Icc 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {a b : α} : IsPreconnected (Set.Icc a b)
• isPreconnected_Ico 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {a b : α} : IsPreconnected (Set.Ico a b)
• isPreconnected_Ioc 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {a b : α} : IsPreconnected (Set.Ioc a b)
• isPreconnected_Ioo 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {a b : α} : IsPreconnected (Set.Ioo a b)
• Set.OrdConnected.isPreconnected 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {s : Set α} (h : s.OrdConnected) : IsPreconnected s
• isPreconnected_iff_ordConnected 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {s : Set α} : IsPreconnected s ↔ s.OrdConnected
• IsPreconnected.Icc_subset 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type v} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set α} (hs : IsPreconnected s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) : Set.Icc a b ⊆ s
• IsPreconnected.eq_univ_of_unbounded 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type v} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set α} (hs : IsPreconnected s) (hb : ¬BddBelow s) (ha : ¬BddAbove s) : s = Set.univ
• IsPreconnected.intermediate_value 📋 Mathlib.Topology.Order.IntermediateValue
  {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set X} (hs : IsPreconnected s) {a b : X} (ha : a ∈ s) (hb : b ∈ s) {f : X → α} (hf : ContinuousOn f s) : Set.Icc (f a) (f b) ⊆ f '' s
• IsPreconnected.Iio_csSup_subset 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] {s : Set α} (hs : IsPreconnected s) (hb : ¬BddBelow s) (ha : BddAbove s) : Set.Iio (sSup s) ⊆ s
• IsPreconnected.Ioi_csInf_subset 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] {s : Set α} (hs : IsPreconnected s) (hb : BddBelow s) (ha : ¬BddAbove s) : Set.Ioi (sInf s) ⊆ s
• IsPreconnected.intermediate_value_Ico 📋 Mathlib.Topology.Order.IntermediateValue
  {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set X} (hs : IsPreconnected s) {a : X} {l : Filter X} (ha : a ∈ s) [l.NeBot] (hl : l ≤ Filter.principal s) {f : X → α} (hf : ContinuousOn f s) {v : α} (ht : Filter.Tendsto f l (nhds v)) : Set.Ico (f a) v ⊆ f '' s
• IsPreconnected.intermediate_value_Ioc 📋 Mathlib.Topology.Order.IntermediateValue
  {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set X} (hs : IsPreconnected s) {a : X} {l : Filter X} (ha : a ∈ s) [l.NeBot] (hl : l ≤ Filter.principal s) {f : X → α} (hf : ContinuousOn f s) {v : α} (ht : Filter.Tendsto f l (nhds v)) : Set.Ioc v (f a) ⊆ f '' s
• IsPreconnected.intermediate_value_Ici 📋 Mathlib.Topology.Order.IntermediateValue
  {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set X} (hs : IsPreconnected s) {a : X} {l : Filter X} (ha : a ∈ s) [l.NeBot] (hl : l ≤ Filter.principal s) {f : X → α} (hf : ContinuousOn f s) (ht : Filter.Tendsto f l Filter.atTop) : Set.Ici (f a) ⊆ f '' s
• IsPreconnected.intermediate_value_Iic 📋 Mathlib.Topology.Order.IntermediateValue
  {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set X} (hs : IsPreconnected s) {a : X} {l : Filter X} (ha : a ∈ s) [l.NeBot] (hl : l ≤ Filter.principal s) {f : X → α} (hf : ContinuousOn f s) (ht : Filter.Tendsto f l Filter.atBot) : Set.Iic (f a) ⊆ f '' s
• IsPreconnected.intermediate_value₂ 📋 Mathlib.Topology.Order.IntermediateValue
  {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set X} (hs : IsPreconnected s) {a b : X} (ha : a ∈ s) (hb : b ∈ s) {f g : X → α} (hf : ContinuousOn f s) (hg : ContinuousOn g s) (ha' : f a ≤ g a) (hb' : g b ≤ f b) : ∃ x ∈ s, f x = g x
• IsPreconnected.intermediate_value_Ioo 📋 Mathlib.Topology.Order.IntermediateValue
  {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set X} (hs : IsPreconnected s) {l₁ l₂ : Filter X} [l₁.NeBot] [l₂.NeBot] (hl₁ : l₁ ≤ Filter.principal s) (hl₂ : l₂ ≤ Filter.principal s) {f : X → α} (hf : ContinuousOn f s) {v₁ v₂ : α} (ht₁ : Filter.Tendsto f l₁ (nhds v₁)) (ht₂ : Filter.Tendsto f l₂ (nhds v₂)) : Set.Ioo v₁ v₂ ⊆ f '' s
• IsPreconnected.intermediate_value_Iii 📋 Mathlib.Topology.Order.IntermediateValue
  {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set X} (hs : IsPreconnected s) {l₁ l₂ : Filter X} [l₁.NeBot] [l₂.NeBot] (hl₁ : l₁ ≤ Filter.principal s) (hl₂ : l₂ ≤ Filter.principal s) {f : X → α} (hf : ContinuousOn f s) (ht₁ : Filter.Tendsto f l₁ Filter.atBot) (ht₂ : Filter.Tendsto f l₂ Filter.atTop) : Set.univ ⊆ f '' s
• IsPreconnected.intermediate_value_Iio 📋 Mathlib.Topology.Order.IntermediateValue
  {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set X} (hs : IsPreconnected s) {l₁ l₂ : Filter X} [l₁.NeBot] [l₂.NeBot] (hl₁ : l₁ ≤ Filter.principal s) (hl₂ : l₂ ≤ Filter.principal s) {f : X → α} (hf : ContinuousOn f s) {v : α} (ht₁ : Filter.Tendsto f l₁ Filter.atBot) (ht₂ : Filter.Tendsto f l₂ (nhds v)) : Set.Iio v ⊆ f '' s
• IsPreconnected.intermediate_value_Ioi 📋 Mathlib.Topology.Order.IntermediateValue
  {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set X} (hs : IsPreconnected s) {l₁ l₂ : Filter X} [l₁.NeBot] [l₂.NeBot] (hl₁ : l₁ ≤ Filter.principal s) (hl₂ : l₂ ≤ Filter.principal s) {f : X → α} (hf : ContinuousOn f s) {v : α} (ht₁ : Filter.Tendsto f l₁ (nhds v)) (ht₂ : Filter.Tendsto f l₂ Filter.atTop) : Set.Ioi v ⊆ f '' s
• IsPreconnected.intermediate_value₂_eventually₁ 📋 Mathlib.Topology.Order.IntermediateValue
  {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set X} (hs : IsPreconnected s) {a : X} {l : Filter X} (ha : a ∈ s) [l.NeBot] (hl : l ≤ Filter.principal s) {f g : X → α} (hf : ContinuousOn f s) (hg : ContinuousOn g s) (ha' : f a ≤ g a) (he : g ≤ᶠ[l] f) : ∃ x ∈ s, f x = g x
• IsPreconnected.intermediate_value₂_eventually₂ 📋 Mathlib.Topology.Order.IntermediateValue
  {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set X} (hs : IsPreconnected s) {l₁ l₂ : Filter X} [l₁.NeBot] [l₂.NeBot] (hl₁ : l₁ ≤ Filter.principal s) (hl₂ : l₂ ≤ Filter.principal s) {f g : X → α} (hf : ContinuousOn f s) (hg : ContinuousOn g s) (he₁ : f ≤ᶠ[l₁] g) (he₂ : g ≤ᶠ[l₂] f) : ∃ x ∈ s, f x = g x
• setOfPred_isPreconnected_subset_of_ordered 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] : {s | IsPreconnected s} ⊆ Set.range (Function.uncurry Set.Icc) ∪ Set.range (Function.uncurry Set.Ico) ∪ Set.range (Function.uncurry Set.Ioc) ∪ Set.range (Function.uncurry Set.Ioo) ∪ (Set.range Set.Ici ∪ Set.range Set.Ioi ∪ Set.range Set.Iic ∪ Set.range Set.Iio ∪ {Set.univ, ∅})
• setOf_isPreconnected_subset_of_ordered 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] : {s | IsPreconnected s} ⊆ Set.range (Function.uncurry Set.Icc) ∪ Set.range (Function.uncurry Set.Ico) ∪ Set.range (Function.uncurry Set.Ioc) ∪ Set.range (Function.uncurry Set.Ioo) ∪ (Set.range Set.Ici ∪ Set.range Set.Ioi ∪ Set.range Set.Iic ∪ Set.range Set.Iio ∪ {Set.univ, ∅})
• setOfPred_isPreconnected_eq_of_ordered 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] : {s | IsPreconnected s} = Set.range (Function.uncurry Set.Icc) ∪ Set.range (Function.uncurry Set.Ico) ∪ Set.range (Function.uncurry Set.Ioc) ∪ Set.range (Function.uncurry Set.Ioo) ∪ (Set.range Set.Ici ∪ Set.range Set.Ioi ∪ Set.range Set.Iic ∪ Set.range Set.Iio ∪ {Set.univ, ∅})
• setOf_isPreconnected_eq_of_ordered 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] : {s | IsPreconnected s} = Set.range (Function.uncurry Set.Icc) ∪ Set.range (Function.uncurry Set.Ico) ∪ Set.range (Function.uncurry Set.Ioc) ∪ Set.range (Function.uncurry Set.Ioo) ∪ (Set.range Set.Ici ∪ Set.range Set.Ioi ∪ Set.range Set.Iic ∪ Set.range Set.Iio ∪ {Set.univ, ∅})
• IsPreconnected.mem_intervals 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] {s : Set α} (hs : IsPreconnected s) : s ∈ {Set.Icc (sInf s) (sSup s), Set.Ico (sInf s) (sSup s), Set.Ioc (sInf s) (sSup s), Set.Ioo (sInf s) (sSup s), Set.Ici (sInf s), Set.Ioi (sInf s), Set.Iic (sSup s), Set.Iio (sSup s), Set.univ, ∅}
• IsPreconnected.measurableSet 📋 Mathlib.MeasureTheory.Constructions.BorelSpace.Order
  {α : Type u_1} {s : Set α} [TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [LinearOrder α] [OrderClosedTopology α] (h : IsPreconnected s) : MeasurableSet s
• IsPreconnected.preperfect_of_nontrivial 📋 Mathlib.Topology.Perfect
  {α : Type u_1} [TopologicalSpace α] [T1Space α] {U : Set α} (hu : U.Nontrivial) (h : IsPreconnected U) : Preperfect U
• Convex.isPreconnected 📋 Mathlib.Analysis.Convex.PathConnected
  {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul ℝ E] {s : Set E} (h : Convex ℝ s) : IsPreconnected s
• IsPreconnected.convex 📋 Mathlib.Analysis.Convex.Topology
  {s : Set ℝ} : IsPreconnected s → Convex ℝ s
• Real.convex_iff_isPreconnected 📋 Mathlib.Analysis.Convex.Topology
  {s : Set ℝ} : Convex ℝ s ↔ IsPreconnected s
• AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq 📋 Mathlib.Analysis.Analytic.Uniqueness
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f g : E → F} {U : Set E} (hf : AnalyticOnNhd 𝕜 f U) (hg : AnalyticOnNhd 𝕜 g U) (hU : IsPreconnected U) {z₀ : E} (h₀ : z₀ ∈ U) (hfg : f =ᶠ[nhds z₀] g) : Set.EqOn f g U
• AnalyticOnNhd.eqOn_zero_of_preconnected_of_eventuallyEq_zero 📋 Mathlib.Analysis.Analytic.Uniqueness
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {U : Set E} (hf : AnalyticOnNhd 𝕜 f U) (hU : IsPreconnected U) {z₀ : E} (h₀ : z₀ ∈ U) (hfz₀ : f =ᶠ[nhds z₀] 0) : Set.EqOn f 0 U
• AnalyticOnNhd.eqOn_zero_of_preconnected_of_eventuallyEq_zero_aux 📋 Mathlib.Analysis.Analytic.Uniqueness
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F} {U : Set E} (hf : AnalyticOnNhd 𝕜 f U) (hU : IsPreconnected U) {z₀ : E} (h₀ : z₀ ∈ U) (hfz₀ : f =ᶠ[nhds z₀] 0) : Set.EqOn f 0 U
• IsOpen.exists_is_const_of_deriv_eq_zero 📋 Mathlib.Analysis.Calculus.MeanValue
  {𝕜 : Type u_3} {G : Type u_4} [RCLike 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : 𝕜 → G} {s : Set 𝕜} (hs : IsOpen s) (hs' : IsPreconnected s) (hf : DifferentiableOn 𝕜 f s) (hf' : Set.EqOn (deriv f) 0 s) : ∃ a, ∀ x ∈ s, f x = a
• IsOpen.is_const_of_deriv_eq_zero 📋 Mathlib.Analysis.Calculus.MeanValue
  {𝕜 : Type u_3} {G : Type u_4} [RCLike 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : 𝕜 → G} {s : Set 𝕜} (hs : IsOpen s) (hs' : IsPreconnected s) (hf : DifferentiableOn 𝕜 f s) (hf' : Set.EqOn (deriv f) 0 s) {x y : 𝕜} (hx : x ∈ s) (hy : y ∈ s) : f x = f y
• IsOpen.eqOn_of_deriv_eq 📋 Mathlib.Analysis.Calculus.MeanValue
  {𝕜 : Type u_3} {G : Type u_4} [RCLike 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {s : Set 𝕜} {x : 𝕜} {f g : 𝕜 → G} (hs : IsOpen s) (hs' : IsPreconnected s) (hf : DifferentiableOn 𝕜 f s) (hg : DifferentiableOn 𝕜 g s) (hf' : Set.EqOn (deriv f) (deriv g) s) (hx : x ∈ s) (hfgx : f x = g x) : Set.EqOn f g s
• IsOpen.exists_eq_add_of_deriv_eq 📋 Mathlib.Analysis.Calculus.MeanValue
  {𝕜 : Type u_3} {G : Type u_4} [RCLike 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {s : Set 𝕜} {f g : 𝕜 → G} (hs : IsOpen s) (hs' : IsPreconnected s) (hf : DifferentiableOn 𝕜 f s) (hg : DifferentiableOn 𝕜 g s) (hf' : Set.EqOn (deriv f) (deriv g) s) : ∃ a, Set.EqOn f (fun x => g x + a) s
• IsOpen.exists_eq_add_of_fderiv_eq 📋 Mathlib.Analysis.Calculus.MeanValue
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedSpace 𝕜 E] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f g : E → G} {s : Set E} (hs : IsOpen s) (hs' : IsPreconnected s) (hf : DifferentiableOn 𝕜 f s) (hg : DifferentiableOn 𝕜 g s) (hf' : Set.EqOn (fderiv 𝕜 f) (fderiv 𝕜 g) s) : ∃ a, Set.EqOn f (fun x => g x + a) s
• IsOpen.eqOn_of_fderiv_eq 📋 Mathlib.Analysis.Calculus.MeanValue
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedSpace 𝕜 E] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f g : E → G} {s : Set E} {x : E} (hs : IsOpen s) (hs' : IsPreconnected s) (hf : DifferentiableOn 𝕜 f s) (hg : DifferentiableOn 𝕜 g s) (hf' : ∀ x ∈ s, fderiv 𝕜 f x = fderiv 𝕜 g x) (hx : x ∈ s) (hfgx : f x = g x) : Set.EqOn f g s
• IsOpen.exists_is_const_of_fderiv_eq_zero 📋 Mathlib.Analysis.Calculus.MeanValue
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedSpace 𝕜 E] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E → G} {s : Set E} (hs : IsOpen s) (hs' : IsPreconnected s) (hf : DifferentiableOn 𝕜 f s) (hf' : Set.EqOn (fderiv 𝕜 f) 0 s) : ∃ a, ∀ x ∈ s, f x = a
• IsOpen.is_const_of_fderiv_eq_zero 📋 Mathlib.Analysis.Calculus.MeanValue
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedSpace 𝕜 E] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E → G} {s : Set E} (hs : IsOpen s) (hs' : IsPreconnected s) (hf : DifferentiableOn 𝕜 f s) (hf' : Set.EqOn (fderiv 𝕜 f) 0 s) {x y : E} (hx : x ∈ s) (hy : y ∈ s) : f x = f y
• AnalyticOnNhd.eqOn_or_eventually_ne_of_preconnected 📋 Mathlib.Analysis.Analytic.IsolatedZeros
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f g : 𝕜 → E} {U : Set 𝕜} (hf : AnalyticOnNhd 𝕜 f U) (hg : AnalyticOnNhd 𝕜 g U) (hU : IsPreconnected U) : Set.EqOn f g U ∨ ∀ᶠ (x : 𝕜) in Filter.codiscreteWithin U, f x ≠ g x
• AnalyticOnNhd.eqOn_zero_or_eventually_ne_zero_of_preconnected 📋 Mathlib.Analysis.Analytic.IsolatedZeros
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜} (hf : AnalyticOnNhd 𝕜 f U) (hU : IsPreconnected U) : Set.EqOn f 0 U ∨ ∀ᶠ (x : 𝕜) in Filter.codiscreteWithin U, f x ≠ 0
• AnalyticOnNhd.eqOn_of_preconnected_of_frequently_eq 📋 Mathlib.Analysis.Analytic.IsolatedZeros
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f g : 𝕜 → E} {z₀ : 𝕜} {U : Set 𝕜} (hf : AnalyticOnNhd 𝕜 f U) (hg : AnalyticOnNhd 𝕜 g U) (hU : IsPreconnected U) (h₀ : z₀ ∈ U) (hfg : ∃ᶠ (z : 𝕜) in nhdsWithin z₀ {z₀}ᶜ, f z = g z) : Set.EqOn f g U
• AnalyticOnNhd.eqOn_of_preconnected_of_mem_closure 📋 Mathlib.Analysis.Analytic.IsolatedZeros
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f g : 𝕜 → E} {z₀ : 𝕜} {U : Set 𝕜} (hf : AnalyticOnNhd 𝕜 f U) (hg : AnalyticOnNhd 𝕜 g U) (hU : IsPreconnected U) (h₀ : z₀ ∈ U) (hfg : z₀ ∈ closure ({z | f z = g z} \ {z₀})) : Set.EqOn f g U
• AnalyticOnNhd.eqOn_zero_of_preconnected_of_frequently_eq_zero 📋 Mathlib.Analysis.Analytic.IsolatedZeros
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜} {U : Set 𝕜} (hf : AnalyticOnNhd 𝕜 f U) (hU : IsPreconnected U) (h₀ : z₀ ∈ U) (hfw : ∃ᶠ (z : 𝕜) in nhdsWithin z₀ {z₀}ᶜ, f z = 0) : Set.EqOn f 0 U
• AnalyticOnNhd.eqOn_zero_of_preconnected_of_mem_closure 📋 Mathlib.Analysis.Analytic.IsolatedZeros
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜} {U : Set 𝕜} (hf : AnalyticOnNhd 𝕜 f U) (hU : IsPreconnected U) (h₀ : z₀ ∈ U) (hfz₀ : z₀ ∈ closure ({z | f z = 0} \ {z₀})) : Set.EqOn f 0 U
• AnalyticOnNhd.eq_zero_or_eq_zero_of_mul_eq_zero 📋 Mathlib.Analysis.Analytic.IsolatedZeros
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} {A : Type u_3} [NormedRing A] [IsDomain A] [NormedAlgebra 𝕜 A] {f g : 𝕜 → A} (hf : AnalyticOnNhd 𝕜 f U) (hg : AnalyticOnNhd 𝕜 g U) (hfg : ∀ z ∈ U, f z * g z = 0) (hU : IsPreconnected U) : (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0
• AnalyticOnNhd.eq_zero_or_eq_zero_of_smul_eq_zero 📋 Mathlib.Analysis.Analytic.IsolatedZeros
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} {A : Type u_3} [NormedRing A] [IsDomain A] [NormedAlgebra 𝕜 A] {B : Type u_4} [NormedAddCommGroup B] [NormedSpace 𝕜 B] [Module A B] [Module.IsTorsionFree A B] {f : 𝕜 → A} {g : 𝕜 → B} (hf : AnalyticOnNhd 𝕜 f U) (hg : AnalyticOnNhd 𝕜 g U) (hfg : ∀ z ∈ U, f z • g z = 0) (hU : IsPreconnected U) : (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0
• logDeriv_eqOn_iff 📋 Mathlib.Analysis.Calculus.LogDeriv
  {𝕜 : Type u_1} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [IsRCLikeNormedField 𝕜] {f g : 𝕜 → 𝕜'} {s : Set 𝕜} (hf : DifferentiableOn 𝕜 f s) (hg : DifferentiableOn 𝕜 g s) (hs2 : IsOpen s) (hsc : IsPreconnected s) (hgn : ∀ x ∈ s, g x ≠ 0) (hfn : ∀ x ∈ s, f x ≠ 0) : Set.EqOn (logDeriv f) (logDeriv g) s ↔ ∃ z, z ≠ 0 ∧ Set.EqOn f (z • g) s
• Metric.isPreconnected_ball 📋 Mathlib.Analysis.Normed.Module.Connected
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {r : ℝ} : IsPreconnected (Metric.ball x r)
• Metric.isPreconnected_closedBall 📋 Mathlib.Analysis.Normed.Module.Connected
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {r : ℝ} : IsPreconnected (Metric.closedBall x r)
• Metric.isPreconnected_closedEBall 📋 Mathlib.Analysis.Normed.Module.Connected
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {r : ENNReal} : IsPreconnected (Metric.closedEBall x r)
• Metric.isPreconnected_eball 📋 Mathlib.Analysis.Normed.Module.Connected
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {r : ENNReal} : IsPreconnected (Metric.eball x r)
• isPreconnected_sphere 📋 Mathlib.Analysis.Normed.Module.Connected
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (h : 1 < Module.rank ℝ E) (x : E) (r : ℝ) : IsPreconnected (Metric.sphere x r)
• AnalyticOnNhd.analyticOrderAt_ne_top_of_isPreconnected 📋 Mathlib.Analysis.Analytic.Order
  {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {U : Set 𝕜} {f : 𝕜 → E} {x y : 𝕜} (hf : AnalyticOnNhd 𝕜 f U) (hU : IsPreconnected U) (h₁x : x ∈ U) (hy : y ∈ U) (h₂x : analyticOrderAt f x ≠ ⊤) : analyticOrderAt f y ≠ ⊤
• TopologicalSpace.vietoris.isPreconnected_nonempty_finite_subsets 📋 Mathlib.Topology.Sets.VietorisTopology
  {α : Type u_1} [TopologicalSpace α] {s : Set α} (hs : IsPreconnected s) : IsPreconnected {t | t.Nonempty ∧ t.Finite ∧ t ⊆ s}
• TopologicalSpace.NonemptyCompacts.isPreconnected_Iic 📋 Mathlib.Topology.Sets.VietorisTopology
  {α : Type u_1} [TopologicalSpace α] {K : TopologicalSpace.NonemptyCompacts α} (hK : IsPreconnected ↑K) : IsPreconnected (Set.Iic K)
• TopologicalSpace.NonemptyCompacts.isPreconnected_subsets 📋 Mathlib.Topology.Sets.VietorisTopology
  {α : Type u_1} [TopologicalSpace α] {s : Set α} (hs : IsPreconnected s) : IsPreconnected {K | ↑K ⊆ s}
• TopologicalSpace.vietoris.isPreconnected_sUnion 📋 Mathlib.Topology.Sets.VietorisTopology
  {α : Type u_1} [TopologicalSpace α] {s : Set (Set α)} (hs : IsPreconnected s) (h : ∃ t ∈ s, IsPreconnected t) : IsPreconnected (⋃₀ s)
• TopologicalSpace.Compacts.isPreconnected_Ioc 📋 Mathlib.Topology.Sets.VietorisTopology
  {α : Type u_1} [TopologicalSpace α] {K L : TopologicalSpace.Compacts α} (hL : IsPreconnected ↑L) : IsPreconnected (Set.Ioc K L)
• TopologicalSpace.NonemptyCompacts.isPreconnected_Icc 📋 Mathlib.Topology.Sets.VietorisTopology
  {α : Type u_1} [TopologicalSpace α] {K L : TopologicalSpace.NonemptyCompacts α} (hL : IsPreconnected ↑L) : IsPreconnected (Set.Icc K L)
• TopologicalSpace.NonemptyCompacts.isPreconnected_Ioc 📋 Mathlib.Topology.Sets.VietorisTopology
  {α : Type u_1} [TopologicalSpace α] {K L : TopologicalSpace.NonemptyCompacts α} (hL : IsPreconnected ↑L) : IsPreconnected (Set.Ioc K L)
• TopologicalSpace.Compacts.isPreconnected_nonempty_subsets 📋 Mathlib.Topology.Sets.VietorisTopology
  {α : Type u_1} [TopologicalSpace α] {s : Set α} (hs : IsPreconnected s) : IsPreconnected {K | (↑K).Nonempty ∧ ↑K ⊆ s}
• TopologicalSpace.NonemptyCompacts.isPreconnected_finite_subsets 📋 Mathlib.Topology.Sets.VietorisTopology
  {α : Type u_1} [TopologicalSpace α] {s : Set α} (hs : IsPreconnected s) : IsPreconnected {K | (↑K).Finite ∧ ↑K ⊆ s}
• TopologicalSpace.Compacts.isPreconnected_Icc 📋 Mathlib.Topology.Sets.VietorisTopology
  {α : Type u_1} [TopologicalSpace α] {K L : TopologicalSpace.Compacts α} (hK : K ≠ ⊥) (hL : IsPreconnected ↑L) : IsPreconnected (Set.Icc K L)
• TopologicalSpace.Compacts.isPreconnected_nonempty_finite_subsets 📋 Mathlib.Topology.Sets.VietorisTopology
  {α : Type u_1} [TopologicalSpace α] {s : Set α} (hs : IsPreconnected s) : IsPreconnected {K | (↑K).Nonempty ∧ (↑K).Finite ∧ ↑K ⊆ s}
• TopologicalSpace.vietoris.isPreconnected_biUnion 📋 Mathlib.Topology.Sets.VietorisTopology
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {f : α → Set β} (hs : IsPreconnected s) (hf : ContinuousOn f s) (h : ∃ x ∈ s, IsPreconnected (f x)) : IsPreconnected (⋃ x ∈ s, f x)
• Subalgebra.spectrum_eq_of_isPreconnected_compl 📋 Mathlib.Analysis.Normed.Algebra.Spectrum
  {𝕜 : Type u_3} {A : Type u_4} {SA : Type u_5} [NormedRing A] [CompleteSpace A] [SetLike SA A] [SubringClass SA A] [NontriviallyNormedField 𝕜] [NormedAlgebra 𝕜 A] [SMulMemClass SA 𝕜 A] (S : SA) [hS : IsClosed ↑S] (x : ↥S) (h : IsPreconnected (spectrum 𝕜 ↑x)ᶜ) : spectrum 𝕜 x = spectrum 𝕜 ↑x
• IsSeparatedMap.eqOn_of_comp_eqOn 📋 Mathlib.Topology.SeparatedMap
  {X : Type u_1} {E : Type u_2} {A : Type u_3} [TopologicalSpace E] [TopologicalSpace A] {p : E → X} {s : Set A} {g₁ g₂ : A → E} (sep : IsSeparatedMap p) (inj : IsLocallyInjective p) (hs : IsPreconnected s) (h₁ : ContinuousOn g₁ s) (h₂ : ContinuousOn g₂ s) (he : Set.EqOn (p ∘ g₁) (p ∘ g₂) s) {a : A} (has : a ∈ s) (ha : g₁ a = g₂ a) : Set.EqOn g₁ g₂ s
• IsSeparatedMap.constOn_of_comp 📋 Mathlib.Topology.SeparatedMap
  {X : Type u_1} {E : Type u_2} {A : Type u_3} [TopologicalSpace E] [TopologicalSpace A] {p : E → X} {s : Set A} {g : A → E} (sep : IsSeparatedMap p) (inj : IsLocallyInjective p) (hs : IsPreconnected s) (cont : ContinuousOn g s) (he : ∀ a ∈ s, ∀ a' ∈ s, p (g a) = p (g a')) {a a' : A} (ha : a ∈ s) (ha' : a' ∈ s) : g a = g a'
• IsCoveringMap.eqOn_of_comp_eqOn 📋 Mathlib.Topology.Covering.Basic
  {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} (hf : IsCoveringMap f) {A : Type u_3} [TopologicalSpace A] {s : Set A} {g₁ g₂ : A → E} (hs : IsPreconnected s) (h₁ : ContinuousOn g₁ s) (h₂ : ContinuousOn g₂ s) (he : Set.EqOn (f ∘ g₁) (f ∘ g₂) s) {a : A} (has : a ∈ s) (ha : g₁ a = g₂ a) : Set.EqOn g₁ g₂ s
• IsCoveringMap.constOn_of_comp 📋 Mathlib.Topology.Covering.Basic
  {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} (hf : IsCoveringMap f) {A : Type u_3} [TopologicalSpace A] {s : Set A} {g : A → E} (hs : IsPreconnected s) (cont : ContinuousOn g s) (he : ∀ a ∈ s, ∀ a' ∈ s, f (g a) = f (g a')) {a a' : A} (ha : a ∈ s) (ha' : a' ∈ s) : g a = g a'
• Circle.not_isPreconnected_compl_pair 📋 Mathlib.Analysis.SpecialFunctions.Complex.Circle
  {x y : Circle} (hxy : x ≠ y) : ¬IsPreconnected {x, y}ᶜ
• cauchy_map_of_uniformCauchySeqOn_fderiv 📋 Mathlib.Analysis.Calculus.UniformLimitsDeriv
  {ι : Type u_1} {l : Filter ι} {E : Type u_2} [NormedAddCommGroup E] {𝕜 : Type u_3} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedSpace 𝕜 E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : ι → E → G} {f' : ι → E → E →L[𝕜] G} {s : Set E} (hs : IsOpen s) (h's : IsPreconnected s) (hf' : UniformCauchySeqOn f' l s) (hf : ∀ (n : ι), ∀ y ∈ s, HasFDerivAt (f n) (f' n y) y) {x₀ x : E} (hx₀ : x₀ ∈ s) (hx : x ∈ s) (hfg : Cauchy (Filter.map (fun n => f n x₀) l)) : Cauchy (Filter.map (fun n => f n x) l)
• summable_of_summable_hasDerivAt_of_isPreconnected 📋 Mathlib.Analysis.Calculus.SmoothSeries
  {α : Type u_1} {𝕜 : Type u_2} {F : Type u_4} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedAddCommGroup F] [CompleteSpace F] {u : α → ℝ} [NormedSpace 𝕜 F] {g g' : α → 𝕜 → F} {t : Set 𝕜} {y₀ y : 𝕜} (hu : Summable u) (ht : IsOpen t) (h't : IsPreconnected t) (hg : ∀ (n : α), ∀ y ∈ t, HasDerivAt (g n) (g' n y) y) (hg' : ∀ (n : α), ∀ y ∈ t, ‖g' n y‖ ≤ u n) (hy₀ : y₀ ∈ t) (hg0 : Summable fun x => g x y₀) (hy : y ∈ t) : Summable fun n => g n y
• hasDerivAt_tsum_of_isPreconnected 📋 Mathlib.Analysis.Calculus.SmoothSeries
  {α : Type u_1} {𝕜 : Type u_2} {F : Type u_4} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedAddCommGroup F] [CompleteSpace F] {u : α → ℝ} [NormedSpace 𝕜 F] {g g' : α → 𝕜 → F} {t : Set 𝕜} {y₀ y : 𝕜} (hu : Summable u) (ht : IsOpen t) (h't : IsPreconnected t) (hg : ∀ (n : α), ∀ y ∈ t, HasDerivAt (g n) (g' n y) y) (hg' : ∀ (n : α), ∀ y ∈ t, ‖g' n y‖ ≤ u n) (hy₀ : y₀ ∈ t) (hg0 : Summable fun n => g n y₀) (hy : y ∈ t) : HasDerivAt (fun z => ∑' (n : α), g n z) (∑' (n : α), g' n y) y
• summable_of_summable_hasFDerivAt_of_isPreconnected 📋 Mathlib.Analysis.Calculus.SmoothSeries
  {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [CompleteSpace F] {u : α → ℝ} [NormedSpace 𝕜 F] {f : α → E → F} {f' : α → E → E →L[𝕜] F} {s : Set E} {x₀ x : E} (hu : Summable u) (hs : IsOpen s) (h's : IsPreconnected s) (hf : ∀ (n : α), ∀ x ∈ s, HasFDerivAt (f n) (f' n x) x) (hf' : ∀ (n : α), ∀ x ∈ s, ‖f' n x‖ ≤ u n) (hx₀ : x₀ ∈ s) (hf0 : Summable fun x => f x x₀) (hx : x ∈ s) : Summable fun n => f n x
• hasFDerivAt_tsum_of_isPreconnected 📋 Mathlib.Analysis.Calculus.SmoothSeries
  {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [CompleteSpace F] {u : α → ℝ} [NormedSpace 𝕜 F] {f : α → E → F} {f' : α → E → E →L[𝕜] F} {s : Set E} {x₀ x : E} (hu : Summable u) (hs : IsOpen s) (h's : IsPreconnected s) (hf : ∀ (n : α), ∀ x ∈ s, HasFDerivAt (f n) (f' n x) x) (hf' : ∀ (n : α), ∀ x ∈ s, ‖f' n x‖ ≤ u n) (hx₀ : x₀ ∈ s) (hf0 : Summable fun n => f n x₀) (hx : x ∈ s) : HasFDerivAt (fun y => ∑' (n : α), f n y) (∑' (n : α), f' n x) x
• Complex.eqOn_closure_of_isPreconnected_of_isMaxOn_norm 📋 Mathlib.Analysis.Complex.AbsMax
  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] {F : Type v} [NormedAddCommGroup F] [NormedSpace ℂ F] [StrictConvexSpace ℝ F] {f : E → F} {U : Set E} {c : E} (hc : IsPreconnected U) (ho : IsOpen U) (hd : DiffContOnCl ℂ f U) (hcU : c ∈ U) (hm : IsMaxOn (norm ∘ f) U c) : Set.EqOn f (Function.const E (f c)) (closure U)
• Complex.norm_eqOn_closure_of_isPreconnected_of_isMaxOn 📋 Mathlib.Analysis.Complex.AbsMax
  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] {F : Type v} [NormedAddCommGroup F] [NormedSpace ℂ F] {f : E → F} {U : Set E} {c : E} (hc : IsPreconnected U) (ho : IsOpen U) (hd : DiffContOnCl ℂ f U) (hcU : c ∈ U) (hm : IsMaxOn (norm ∘ f) U c) : Set.EqOn (norm ∘ f) (Function.const E ‖f c‖) (closure U)
• Complex.eqOn_of_isPreconnected_of_isMaxOn_norm 📋 Mathlib.Analysis.Complex.AbsMax
  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] {F : Type v} [NormedAddCommGroup F] [NormedSpace ℂ F] [StrictConvexSpace ℝ F] {f : E → F} {U : Set E} {c : E} (hc : IsPreconnected U) (ho : IsOpen U) (hd : DifferentiableOn ℂ f U) (hcU : c ∈ U) (hm : IsMaxOn (norm ∘ f) U c) : Set.EqOn f (Function.const E (f c)) U
• Complex.norm_eqOn_of_isPreconnected_of_isMaxOn 📋 Mathlib.Analysis.Complex.AbsMax
  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] {F : Type v} [NormedAddCommGroup F] [NormedSpace ℂ F] {f : E → F} {U : Set E} {c : E} (hc : IsPreconnected U) (ho : IsOpen U) (hd : DifferentiableOn ℂ f U) (hcU : c ∈ U) (hm : IsMaxOn (norm ∘ f) U c) : Set.EqOn (norm ∘ f) (Function.const E ‖f c‖) U
• MeromorphicOn.meromorphicOrderAt_eq_top_of_isPreconnected 📋 Mathlib.Analysis.Meromorphic.Order
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} {U : Set 𝕜} (hf : MeromorphicOn f U) {y : 𝕜} (hU : IsPreconnected U) (h₁x : x ∈ U) (hy : y ∈ U) (h₂x : meromorphicOrderAt f x = ⊤) : meromorphicOrderAt f y = ⊤
• MeromorphicOn.meromorphicOrderAt_ne_top_of_isPreconnected 📋 Mathlib.Analysis.Meromorphic.Order
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} {U : Set 𝕜} (hf : MeromorphicOn f U) {y : 𝕜} (hU : IsPreconnected U) (h₁x : x ∈ U) (hy : y ∈ U) (h₂x : meromorphicOrderAt f x ≠ ⊤) : meromorphicOrderAt f y ≠ ⊤
• MeromorphicOn.mul_inv_eventuallyEq 📋 Mathlib.Analysis.Meromorphic.Order
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {𝕜' : Type u_4} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {U : Set 𝕜} {f : 𝕜 → 𝕜'} (hf : MeromorphicOn f U) (hU : IsPreconnected U) (h0 : ¬f =ᶠ[Filter.codiscreteWithin U] 0) : f * f⁻¹ =ᶠ[Filter.codiscreteWithin U] 1
• AnalyticOnNhd.is_constant_or_isOpen 📋 Mathlib.Analysis.Complex.OpenMapping
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {U : Set E} {g : E → ℂ} (hg : AnalyticOnNhd ℂ g U) (hU : IsPreconnected U) : (∃ w, ∀ z ∈ U, g z = w) ∨ ∀ s ⊆ U, IsOpen s → IsOpen (g '' s)
• QuasiconcaveOn.isPreconnected_preimage_subtype 📋 Mathlib.Analysis.Convex.Quasiconvex
  {E : Type u_4} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] {β : Type u_5} [Preorder β] {f : E → β} {s : Set E} {t : β} (hfc : QuasiconcaveOn ℝ s f) : IsPreconnected (Subtype.val ⁻¹' f ⁻¹' Set.Ici t)
• QuasiconvexOn.isPreconnected_preimage_subtype 📋 Mathlib.Analysis.Convex.Quasiconvex
  {E : Type u_4} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] {β : Type u_5} [Preorder β] {f : E → β} {s : Set E} {t : β} (hfc : QuasiconvexOn ℝ s f) : IsPreconnected (Subtype.val ⁻¹' f ⁻¹' Set.Iic t)
• QuasilinearOn.isPreconnected_preimage_subtype 📋 Mathlib.Analysis.Convex.Quasiconvex
  {E : Type u_4} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] {β : Type u_5} [Preorder β] {f : E → β} {s : Set E} {t : β} (hfc : QuasilinearOn ℝ s f) : IsPreconnected (Subtype.val ⁻¹' f ⁻¹' Set.Iic t)
• AffineSubspace.isPreconnected_setOfPred_sOppSide 📋 Mathlib.Analysis.Convex.Side
  {V : Type u_2} {P : Type u_4} [SeminormedAddCommGroup V] [NormedSpace ℝ V] [PseudoMetricSpace P] [NormedAddTorsor V P] (s : AffineSubspace ℝ P) (x : P) : IsPreconnected {y | s.SOppSide x y}
• AffineSubspace.isPreconnected_setOfPred_sSameSide 📋 Mathlib.Analysis.Convex.Side
  {V : Type u_2} {P : Type u_4} [SeminormedAddCommGroup V] [NormedSpace ℝ V] [PseudoMetricSpace P] [NormedAddTorsor V P] (s : AffineSubspace ℝ P) (x : P) : IsPreconnected {y | s.SSameSide x y}
• AffineSubspace.isPreconnected_setOfPred_wOppSide 📋 Mathlib.Analysis.Convex.Side
  {V : Type u_2} {P : Type u_4} [SeminormedAddCommGroup V] [NormedSpace ℝ V] [PseudoMetricSpace P] [NormedAddTorsor V P] (s : AffineSubspace ℝ P) (x : P) : IsPreconnected {y | s.WOppSide x y}
• AffineSubspace.isPreconnected_setOfPred_wSameSide 📋 Mathlib.Analysis.Convex.Side
  {V : Type u_2} {P : Type u_4} [SeminormedAddCommGroup V] [NormedSpace ℝ V] [PseudoMetricSpace P] [NormedAddTorsor V P] (s : AffineSubspace ℝ P) (x : P) : IsPreconnected {y | s.WSameSide x y}
• AffineSubspace.isPreconnected_setOf_sOppSide 📋 Mathlib.Analysis.Convex.Side
  {V : Type u_2} {P : Type u_4} [SeminormedAddCommGroup V] [NormedSpace ℝ V] [PseudoMetricSpace P] [NormedAddTorsor V P] (s : AffineSubspace ℝ P) (x : P) : IsPreconnected {y | s.SOppSide x y}
• AffineSubspace.isPreconnected_setOf_sSameSide 📋 Mathlib.Analysis.Convex.Side
  {V : Type u_2} {P : Type u_4} [SeminormedAddCommGroup V] [NormedSpace ℝ V] [PseudoMetricSpace P] [NormedAddTorsor V P] (s : AffineSubspace ℝ P) (x : P) : IsPreconnected {y | s.SSameSide x y}
• AffineSubspace.isPreconnected_setOf_wOppSide 📋 Mathlib.Analysis.Convex.Side
  {V : Type u_2} {P : Type u_4} [SeminormedAddCommGroup V] [NormedSpace ℝ V] [PseudoMetricSpace P] [NormedAddTorsor V P] (s : AffineSubspace ℝ P) (x : P) : IsPreconnected {y | s.WOppSide x y}
• AffineSubspace.isPreconnected_setOf_wSameSide 📋 Mathlib.Analysis.Convex.Side
  {V : Type u_2} {P : Type u_4} [SeminormedAddCommGroup V] [NormedSpace ℝ V] [PseudoMetricSpace P] [NormedAddTorsor V P] (s : AffineSubspace ℝ P) (x : P) : IsPreconnected {y | s.WSameSide x y}
• IsPreconnected.infinite_of_nontrivial 📋 Mathlib.Topology.Separation.Connected
  {X : Type u_1} [TopologicalSpace X] [T1Space X] {s : Set X} (h : IsPreconnected s) (hs : s.Nontrivial) : s.Infinite
• MDifferentiableOn.apply_eq_of_isPreconnected_isCompact_isOpen 📋 Mathlib.Geometry.Manifold.Complex
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℂ E H} [I.Boundaryless] {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {f : M → F} {U : Set M} {a b : M} (hd : MDiff[U] f) (hpc : IsPreconnected U) (hc : IsCompact U) (ho : IsOpen U) (ha : a ∈ U) (hb : b ∈ U) : f a = f b
• MDifferentiableOn.eqOn_of_isPreconnected_of_isMaxOn_norm 📋 Mathlib.Geometry.Manifold.Complex
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℂ E H} [I.Boundaryless] {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [StrictConvexSpace ℝ F] {f : M → F} {U : Set M} {c : M} (hd : MDiff[U] f) (hc : IsPreconnected U) (ho : IsOpen U) (hcU : c ∈ U) (hm : IsMaxOn (norm ∘ f) U c) : Set.EqOn f (Function.const M (f c)) U
• MDifferentiableOn.norm_eqOn_of_isPreconnected_of_isMaxOn 📋 Mathlib.Geometry.Manifold.Complex
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℂ E H} [I.Boundaryless] {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {f : M → F} {U : Set M} {c : M} (hd : MDiff[U] f) (hc : IsPreconnected U) (ho : IsOpen U) (hcU : c ∈ U) (hm : IsMaxOn (norm ∘ f) U c) : Set.EqOn (norm ∘ f) (Function.const M ‖f c‖) U
• IsPreconnected.inter_derivedSet_nonempty 📋 Mathlib.Topology.DerivedSet
  {X : Type u_1} [TopologicalSpace X] [T1Space X] {U : Set X} (hs : IsPreconnected U) (a b : Set X) (h : U ⊆ a ∪ b) (ha : (U ∩ derivedSet a).Nonempty) (hb : (U ∩ derivedSet b).Nonempty) : (U ∩ (derivedSet a ∩ derivedSet b)).Nonempty
• eq_of_germ_isConstant_on 📋 Mathlib.Topology.Germ
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} {x : X} {s : Set X} (h : ∀ x ∈ s, (↑f).IsConstant) (hs : IsPreconnected s) {x' : X} (x_in : x ∈ s) (x'_in : x' ∈ s) : f x = f x'

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision 69fae59