Loogle!

Result

Found 236 declarations mentioning R1Space. Of these, only the first 200 are shown.

• R1Space 📋 Mathlib.Topology.Separation.Basic
  (X : Type u_3) [TopologicalSpace X] : Prop
• instR0Space 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R1Space X] : R0Space X
• WeaklyLocallyCompactSpace.locallyCompactSpace 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R1Space X] [WeaklyLocallyCompactSpace X] : LocallyCompactSpace X
• Filter.coclosedCompact_eq_cocompact 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R1Space X] : Filter.coclosedCompact X = Filter.cocompact X
• instR1SpaceSubtype 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R1Space X] (p : X → Prop) : R1Space (Subtype p)
• R1Space.induced 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [R1Space X] (f : Y → X) : R1Space Y
• instLocallyCompactPairOfWeaklyLocallyCompactSpaceOfR1Space 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [WeaklyLocallyCompactSpace X] [TopologicalSpace Y] [R1Space Y] : LocallyCompactPair X Y
• Bornology.relativelyCompact_eq_inCompact 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R1Space X] : Bornology.relativelyCompact X = Bornology.inCompact X
• IsCompact.closure 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R1Space X] {K : Set X} (hK : IsCompact K) : IsCompact (closure K)
• Topology.IsInducing.r1Space 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace Y] {f : Y → X} (hf : Topology.IsInducing f) : R1Space Y
• instR1SpaceForall 📋 Mathlib.Topology.Separation.Basic
  {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), R1Space (X i)] : R1Space ((i : ι) → X i)
• instR1SpaceProd 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace Y] [R1Space Y] : R1Space (X × Y)
• Inseparable.of_nhds_neBot 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R1Space X] {x y : X} (h : (nhds x ⊓ nhds y).NeBot) : Inseparable x y
• IsCompact.closure_of_subset 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R1Space X] {s K : Set X} (hK : IsCompact K) (h : s ⊆ K) : IsCompact (closure s)
• R1Space.iInf 📋 Mathlib.Topology.Separation.Basic
  {ι : Type u_3} {X : Type u_4} {t : ι → TopologicalSpace X} (ht : ∀ (i : ι), R1Space X) : R1Space X
• R1Space.inf 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_3} {t₁ t₂ : TopologicalSpace X} (h₁ : R1Space X) (h₂ : R1Space X) : R1Space X
• exists_isCompact_superset_iff 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R1Space X] {s : Set X} : (∃ K, IsCompact K ∧ s ⊆ K) ↔ IsCompact (closure s)
• isClosed_setOfPred_inseparable 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R1Space X] : IsClosed {p | Inseparable p.1 p.2}
• isClosed_setOfPred_specializes 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R1Space X] : IsClosed {p | p.1 ⤳ p.2}
• isClosed_setOf_inseparable 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R1Space X] : IsClosed {p | Inseparable p.1 p.2}
• isClosed_setOf_specializes 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R1Space X] : IsClosed {p | p.1 ⤳ p.2}
• R1Space.of_continuous_specializes_imp 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace Y] {f : Y → X} (hc : Continuous f) (hspec : ∀ (x y : Y), f x ⤳ f y → x ⤳ y) : R1Space Y
• IsCompact.closure_subset_of_isOpen 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R1Space X] {K : Set X} (hK : IsCompact K) {U : Set X} (hU : IsOpen U) (hKU : K ⊆ U) : closure K ⊆ U
• exists_isOpen_mem_isCompact_closure 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R1Space X] [WeaklyLocallyCompactSpace X] (x : X) : ∃ U, IsOpen U ∧ x ∈ U ∧ IsCompact (closure U)
• exists_mem_nhds_isCompact_isClosed 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R1Space X] [WeaklyLocallyCompactSpace X] (x : X) : ∃ K ∈ nhds x, IsCompact K ∧ IsClosed K
• tendsto_nhds_unique_inseparable 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [R1Space X] {f : Y → X} {l : Filter Y} {a b : X} [l.NeBot] (ha : Filter.Tendsto f l (nhds a)) (hb : Filter.Tendsto f l (nhds b)) : Inseparable a b
• exists_isOpen_superset_and_isCompact_closure 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R1Space X] [WeaklyLocallyCompactSpace X] {K : Set X} (hK : IsCompact K) : ∃ V, IsOpen V ∧ K ⊆ V ∧ IsCompact (closure V)
• R1Space.sInf 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_3} {T : Set (TopologicalSpace X)} (hT : ∀ t ∈ T, R1Space X) : R1Space X
• IsCompact.mem_closure_iff_exists_inseparable 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R1Space X] {y : X} {K : Set X} (hK : IsCompact K) : y ∈ closure K ↔ ∃ x ∈ K, Inseparable x y
• R1Space.mk 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_3} [TopologicalSpace X] (specializes_or_disjoint_nhds : ∀ (x y : X), x ⤳ y ∨ Disjoint (nhds x) (nhds y)) : R1Space X
• R1Space.specializes_or_disjoint_nhds 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_3} {inst✝ : TopologicalSpace X} [self : R1Space X] (x y : X) : x ⤳ y ∨ Disjoint (nhds x) (nhds y)
• disjoint_nhds_nhds_iff_not_inseparable 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R1Space X] {x y : X} : Disjoint (nhds x) (nhds y) ↔ ¬Inseparable x y
• disjoint_nhds_nhds_iff_not_specializes 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R1Space X] {x y : X} : Disjoint (nhds x) (nhds y) ↔ ¬x ⤳ y
• r1Space_iff_inseparable_or_disjoint_nhds 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_3} [TopologicalSpace X] : R1Space X ↔ ∀ (x y : X), Inseparable x y ∨ Disjoint (nhds x) (nhds y)
• r1Space_iff_specializes_or_disjoint_nhds 📋 Mathlib.Topology.Separation.Basic
  (X : Type u_3) [TopologicalSpace X] : R1Space X ↔ ∀ (x y : X), x ⤳ y ∨ Disjoint (nhds x) (nhds y)
• specializes_iff_not_disjoint 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R1Space X] {x y : X} : x ⤳ y ↔ ¬Disjoint (nhds x) (nhds y)
• isCompact_isClosed_basis_nhds 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R1Space X] [WeaklyLocallyCompactSpace X] (x : X) : (nhds x).HasBasis (fun K => K ∈ nhds x ∧ IsCompact K ∧ IsClosed K) fun x => x
• IsCompact.closure_eq_biUnion_inseparable 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R1Space X] {K : Set X} (hK : IsCompact K) : closure K = ⋃ x ∈ K, {y | Inseparable x y}
• IsCompact.closure_eq_biUnion_closure_singleton 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R1Space X] {K : Set X} (hK : IsCompact K) : closure K = ⋃ x ∈ K, closure {x}
• IsCompact.isCompact_isClosed_basis_nhds 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R1Space X] {x : X} {L : Set X} (hLc : IsCompact L) (hxL : L ∈ nhds x) : (nhds x).HasBasis (fun K => K ∈ nhds x ∧ IsCompact K ∧ IsClosed K) fun x => x
• SeparatedNhds.of_isCompact_isCompact_isClosed 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R1Space X] {K L : Set X} (hK : IsCompact K) (hL : IsCompact L) (h'L : IsClosed L) (hd : Disjoint K L) : SeparatedNhds K L
• exists_mem_nhds_isCompact_mapsTo_of_isCompact_mem_nhds 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [R1Space Y] {f : X → Y} {x : X} {K : Set X} {s : Set Y} (hf : Continuous f) (hs : s ∈ nhds (f x)) (hKc : IsCompact K) (hKx : K ∈ nhds x) : ∃ L ∈ nhds x, IsCompact L ∧ Set.MapsTo f L s
• IsCompact.binary_compact_cover 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R1Space X] {K U V : Set X} (hK : IsCompact K) (hU : IsOpen U) (hV : IsOpen V) (h2K : K ⊆ U ∪ V) : ∃ K₁ K₂, IsCompact K₁ ∧ IsCompact K₂ ∧ K₁ ⊆ U ∧ K₂ ⊆ V ∧ K = K₁ ∪ K₂
• r1_separation 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R1Space X] {x y : X} (h : ¬Inseparable x y) : ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v
• IsCompact.finite_compact_cover 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R1Space X] {s : Set X} (hs : IsCompact s) {ι : Type u_3} (t : Finset ι) (U : ι → Set X) (hU : ∀ i ∈ t, IsOpen (U i)) (hsC : s ⊆ ⋃ i ∈ t, U i) : ∃ K, (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i
• T2Space.r1Space 📋 Mathlib.Topology.Separation.Hausdorff
  {X : Type u_1} [TopologicalSpace X] [T2Space X] : R1Space X
• instT2SpaceOfR1SpaceOfT0Space 📋 Mathlib.Topology.Separation.Hausdorff
  {X : Type u_1} [TopologicalSpace X] [R1Space X] [T0Space X] : T2Space X
• R1Space.t2Space_iff_t0Space 📋 Mathlib.Topology.Separation.Hausdorff
  {X : Type u_1} [TopologicalSpace X] [R1Space X] : T2Space X ↔ T0Space X
• SeparationQuotient.t2Space 📋 Mathlib.Topology.Separation.Hausdorff
  {X : Type u_1} [TopologicalSpace X] [R1Space X] : T2Space (SeparationQuotient X)
• SeparationQuotient.t2Space_iff 📋 Mathlib.Topology.Separation.Hausdorff
  {X : Type u_1} [TopologicalSpace X] : T2Space (SeparationQuotient X) ↔ R1Space X
• isPreirreducible_iff_forall_mem_subset_closure_singleton 📋 Mathlib.Topology.Separation.Hausdorff
  {X : Type u_1} [TopologicalSpace X] [R1Space X] {S : Set X} : IsPreirreducible S ↔ ∀ x ∈ S, S ⊆ closure {x}
• Pi.isCompact_closure_iff 📋 Mathlib.Topology.Separation.Hausdorff
  {ι : Type u_4} {X : ι → Type u_5} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), R1Space (X i)] {s : Set ((i : ι) → X i)} : IsCompact (closure s) ↔ ∀ (i : ι), IsCompact (closure (Function.eval i '' s))
• SeparatedNhds.of_isClosed_isCompact_closure_compl_isClosed 📋 Mathlib.Topology.Separation.Hausdorff
  {X : Type u_1} [TopologicalSpace X] [R1Space X] {s t : Set X} (H1 : IsClosed s) (H2 : IsCompact (closure sᶜ)) (H3 : IsClosed t) (H4 : Disjoint s t) : SeparatedNhds s t
• instR1Space 📋 Mathlib.Topology.Separation.Regular
  {X : Type u_1} [TopologicalSpace X] [RegularSpace X] : R1Space X
• instRegularSpaceOfWeaklyLocallyCompactSpaceOfR1Space 📋 Mathlib.Topology.Separation.Regular
  {X : Type u_1} [TopologicalSpace X] [WeaklyLocallyCompactSpace X] [R1Space X] : RegularSpace X
• NormalSpace.of_compactSpace_r1Space 📋 Mathlib.Topology.Separation.Regular
  {X : Type u_1} [TopologicalSpace X] [CompactSpace X] [R1Space X] : NormalSpace X
• IsDenseInducing.inseparable_extend 📋 Mathlib.Topology.DenseEmbedding
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] {i : α → β} [TopologicalSpace γ] [R1Space γ] (di : IsDenseInducing i) {f : α → γ} {a : α} (hf : ContinuousAt f a) : Inseparable (di.extend f (i a)) (f a)
• HasCompactMulSupport.of_mulSupport_subset_isCompact 📋 Mathlib.Topology.Algebra.Support
  {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [One β] {f : α → β} {K : Set α} [R1Space α] (hK : IsCompact K) (h : Function.mulSupport f ⊆ K) : HasCompactMulSupport f
• HasCompactSupport.of_support_subset_isCompact 📋 Mathlib.Topology.Algebra.Support
  {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [Zero β] {f : α → β} {K : Set α} [R1Space α] (hK : IsCompact K) (h : Function.support f ⊆ K) : HasCompactSupport f
• HasCompactMulSupport.intro 📋 Mathlib.Topology.Algebra.Support
  {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [One β] {f : α → β} {K : Set α} [R1Space α] (hK : IsCompact K) (hfK : ∀ x ∉ K, f x = 1) : HasCompactMulSupport f
• HasCompactSupport.intro 📋 Mathlib.Topology.Algebra.Support
  {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [Zero β] {f : α → β} {K : Set α} [R1Space α] (hK : IsCompact K) (hfK : ∀ x ∉ K, f x = 0) : HasCompactSupport f
• exists_compact_iff_hasCompactMulSupport 📋 Mathlib.Topology.Algebra.Support
  {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [One β] {f : α → β} [R1Space α] : (∃ K, IsCompact K ∧ ∀ x ∉ K, f x = 1) ↔ HasCompactMulSupport f
• exists_compact_iff_hasCompactSupport 📋 Mathlib.Topology.Algebra.Support
  {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [Zero β] {f : α → β} [R1Space α] : (∃ K, IsCompact K ∧ ∀ x ∉ K, f x = 0) ↔ HasCompactSupport f
• IsOpen.exists_positiveCompacts_closure_subset 📋 Mathlib.Topology.Sets.Compacts
  {α : Type u_1} [TopologicalSpace α] [R1Space α] [LocallyCompactSpace α] {U : Set α} (ho : IsOpen U) (hn : U.Nonempty) : ∃ K, closure ↑K ⊆ U
• R1Space.quasiSober 📋 Mathlib.Topology.Sober
  {α : Type u_1} [TopologicalSpace α] [R1Space α] : QuasiSober α
• IsCompact.closure_subset_measurableSet 📋 Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
  {γ : Type u_3} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [R1Space γ] {K s : Set γ} (hK : IsCompact K) (hs : MeasurableSet s) (hKs : K ⊆ s) : closure K ⊆ s
• IsCompact.measure_closure 📋 Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
  {γ : Type u_3} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [R1Space γ] {K : Set γ} (hK : IsCompact K) (μ : MeasureTheory.Measure γ) : μ (closure K) = μ K
• instIsMeasurablyGeneratedCocompactOfR1Space 📋 Mathlib.MeasureTheory.Constructions.BorelSpace.Order
  {α : Type u_1} [TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [R1Space α] : (Filter.cocompact α).IsMeasurablyGenerated
• MeasureTheory.Measure.Regular.weaklyRegular 📋 Mathlib.MeasureTheory.Measure.Regular
  {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [R1Space α] [μ.Regular] : μ.WeaklyRegular
• MeasureTheory.Measure.InnerRegularCompactLTTop.instRegularOfBorelSpaceOfR1SpaceOfIsFiniteMeasure 📋 Mathlib.MeasureTheory.Measure.Regular
  {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [BorelSpace α] [R1Space α] [h : μ.InnerRegularCompactLTTop] [MeasureTheory.IsFiniteMeasure μ] : μ.Regular
• MeasureTheory.Measure.InnerRegularCompactLTTop.instWeaklyRegularOfBorelSpaceOfR1SpaceOfIsFiniteMeasure 📋 Mathlib.MeasureTheory.Measure.Regular
  {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [BorelSpace α] [R1Space α] [μ.InnerRegularCompactLTTop] [MeasureTheory.IsFiniteMeasure μ] : μ.WeaklyRegular
• MeasureTheory.Measure.InnerRegular.innerRegularWRT_isClosed_isOpen 📋 Mathlib.MeasureTheory.Measure.Regular
  {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [R1Space α] [OpensMeasurableSpace α] [h : μ.InnerRegular] : μ.InnerRegularWRT IsClosed IsOpen
• MeasureTheory.Measure.Regular.restrict_of_measure_ne_top 📋 Mathlib.MeasureTheory.Measure.Regular
  {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [R1Space α] [BorelSpace α] [μ.Regular] {A : Set α} (h'A : μ A ≠ ⊤) : (μ.restrict A).Regular
• MeasureTheory.Measure.OuterRegular.measure_closure_eq_of_isCompact 📋 Mathlib.MeasureTheory.Measure.Regular
  {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [R1Space α] [μ.OuterRegular] {k : Set α} (hk : IsCompact k) : μ (closure k) = μ k
• IsCompact.exists_isOpen_lt_of_lt 📋 Mathlib.MeasureTheory.Measure.Regular
  {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [μ.InnerRegularCompactLTTop] [MeasureTheory.IsLocallyFiniteMeasure μ] [R1Space α] [BorelSpace α] {K : Set α} (hK : IsCompact K) (r : ENNReal) (hr : μ K < r) : ∃ U, K ⊆ U ∧ IsOpen U ∧ μ U < r
• IsCompact.exists_isOpen_lt_add 📋 Mathlib.MeasureTheory.Measure.Regular
  {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [μ.InnerRegularCompactLTTop] [MeasureTheory.IsLocallyFiniteMeasure μ] [R1Space α] [BorelSpace α] {K : Set α} (hK : IsCompact K) {ε : ENNReal} (hε : ε ≠ 0) : ∃ U, K ⊆ U ∧ IsOpen U ∧ μ U < μ K + ε
• MeasurableSet.exists_isCompact_isClosed_diff_lt 📋 Mathlib.MeasureTheory.Measure.Regular
  {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [BorelSpace α] [R1Space α] [μ.InnerRegularCompactLTTop] ⦃A : Set α⦄ (hA : MeasurableSet A) (h'A : μ A ≠ ⊤) {ε : ENNReal} (hε : ε ≠ 0) : ∃ K ⊆ A, IsCompact K ∧ IsClosed K ∧ μ (A \ K) < ε
• MeasurableSet.exists_isCompact_isClosed_sdiff_lt 📋 Mathlib.MeasureTheory.Measure.Regular
  {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [BorelSpace α] [R1Space α] [μ.InnerRegularCompactLTTop] ⦃A : Set α⦄ (hA : MeasurableSet A) (h'A : μ A ≠ ⊤) {ε : ENNReal} (hε : ε ≠ 0) : ∃ K ⊆ A, IsCompact K ∧ IsClosed K ∧ μ (A \ K) < ε
• MeasurableSet.exists_isCompact_isClosed_lt_add 📋 Mathlib.MeasureTheory.Measure.Regular
  {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [μ.InnerRegularCompactLTTop] [R1Space α] [BorelSpace α] ⦃A : Set α⦄ (hA : MeasurableSet A) (h'A : μ A ≠ ⊤) {ε : ENNReal} (hε : ε ≠ 0) : ∃ K ⊆ A, IsCompact K ∧ IsClosed K ∧ μ A < μ K + ε
• IsCompact.measure_eq_iInf_isOpen 📋 Mathlib.MeasureTheory.Measure.Regular
  {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [μ.InnerRegularCompactLTTop] [MeasureTheory.IsLocallyFiniteMeasure μ] [R1Space α] [BorelSpace α] {K : Set α} (hK : IsCompact K) : μ K = ⨅ U, ⨅ (_ : K ⊆ U), ⨅ (_ : IsOpen U), μ U
• MeasurableSet.exists_isOpen_symmDiff_lt 📋 Mathlib.MeasureTheory.Measure.Regular
  {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [μ.InnerRegularCompactLTTop] [MeasureTheory.IsLocallyFiniteMeasure μ] [R1Space α] [BorelSpace α] {s : Set α} (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) {ε : ENNReal} (hε : ε ≠ 0) : ∃ U, IsOpen U ∧ μ U < ⊤ ∧ μ (symmDiff U s) < ε
• MeasureTheory.NullMeasurableSet.exists_isOpen_symmDiff_lt 📋 Mathlib.MeasureTheory.Measure.Regular
  {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [μ.InnerRegularCompactLTTop] [MeasureTheory.IsLocallyFiniteMeasure μ] [R1Space α] [BorelSpace α] {s : Set α} (hs : MeasureTheory.NullMeasurableSet s μ) (hμs : μ s ≠ ⊤) {ε : ENNReal} (hε : ε ≠ 0) : ∃ U, IsOpen U ∧ μ U < ⊤ ∧ μ (symmDiff U s) < ε
• ContinuousMap.instR1Space 📋 Mathlib.Topology.CompactOpen
  {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [R1Space Y] : R1Space C(X, Y)
• MeasureTheory.Content.measure 📋 Mathlib.MeasureTheory.Measure.Content
  {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] [S : MeasurableSpace G] [BorelSpace G] : MeasureTheory.Measure G
• MeasureTheory.Content.outerRegular 📋 Mathlib.MeasureTheory.Measure.Content
  {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] [S : MeasurableSpace G] [BorelSpace G] : μ.measure.OuterRegular
• MeasureTheory.Content.borel_le_caratheodory 📋 Mathlib.MeasureTheory.Measure.Content
  {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] [S : MeasurableSpace G] [BorelSpace G] : S ≤ μ.outerMeasure.caratheodory
• MeasureTheory.Content.regular 📋 Mathlib.MeasureTheory.Measure.Content
  {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] [S : MeasurableSpace G] [BorelSpace G] [WeaklyLocallyCompactSpace G] : μ.measure.Regular
• MeasureTheory.Content.outerMeasure_of_isOpen 📋 Mathlib.MeasureTheory.Measure.Content
  {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] (U : Set G) (hU : IsOpen U) : μ.outerMeasure U = μ.innerContent { carrier := U, is_open' := hU }
• MeasureTheory.Content.outerMeasure_opens 📋 Mathlib.MeasureTheory.Measure.Content
  {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] (U : TopologicalSpace.Opens G) : μ.outerMeasure ↑U = μ.innerContent U
• MeasureTheory.Content.outerMeasure_lt_top_of_isCompact 📋 Mathlib.MeasureTheory.Measure.Content
  {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] [WeaklyLocallyCompactSpace G] {K : Set G} (hK : IsCompact K) : μ.outerMeasure K < ⊤
• MeasureTheory.Content.le_outerMeasure_compacts 📋 Mathlib.MeasureTheory.Measure.Content
  {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] (K : TopologicalSpace.Compacts G) : μ K ≤ μ.outerMeasure ↑K
• MeasureTheory.Content.outerMeasure_interior_compacts 📋 Mathlib.MeasureTheory.Measure.Content
  {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] (K : TopologicalSpace.Compacts G) : μ.outerMeasure (interior ↑K) ≤ μ K
• MeasureTheory.Content.measure_apply 📋 Mathlib.MeasureTheory.Measure.Content
  {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] [S : MeasurableSpace G] [BorelSpace G] {s : Set G} (hs : MeasurableSet s) : μ.measure s = μ.outerMeasure s
• MeasureTheory.Content.innerContent_iUnion_nat 📋 Mathlib.MeasureTheory.Measure.Content
  {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] ⦃U : ℕ → Set G⦄ (hU : ∀ (i : ℕ), IsOpen (U i)) : μ.innerContent { carrier := ⋃ i, U i, is_open' := ⋯ } ≤ ∑' (i : ℕ), μ.innerContent { carrier := U i, is_open' := ⋯ }
• MeasureTheory.Content.innerContent_iSup_nat 📋 Mathlib.MeasureTheory.Measure.Content
  {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] (U : ℕ → TopologicalSpace.Opens G) : μ.innerContent (⨆ i, U i) ≤ ∑' (i : ℕ), μ.innerContent (U i)
• MeasureTheory.Content.measure_eq_content_of_regular 📋 Mathlib.MeasureTheory.Measure.Content
  {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) [MeasurableSpace G] [R1Space G] [BorelSpace G] (H : μ.ContentRegular) (K : TopologicalSpace.Compacts G) : μ.measure ↑K = μ K
• MeasureTheory.Content.outerMeasure_le 📋 Mathlib.MeasureTheory.Measure.Content
  {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] (U : TopologicalSpace.Opens G) (K : TopologicalSpace.Compacts G) (hUK : ↑U ⊆ ↑K) : μ.outerMeasure ↑U ≤ μ K
• MeasureTheory.Content.outerMeasure_eq_iInf 📋 Mathlib.MeasureTheory.Measure.Content
  {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] (A : Set G) : μ.outerMeasure A = ⨅ U, ⨅ (hU : IsOpen U), ⨅ (_ : A ⊆ U), μ.innerContent { carrier := U, is_open' := hU }
• MeasureTheory.Content.outerMeasure_exists_open 📋 Mathlib.MeasureTheory.Measure.Content
  {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] {A : Set G} (hA : μ.outerMeasure A ≠ ⊤) {ε : NNReal} (hε : ε ≠ 0) : ∃ U, A ⊆ ↑U ∧ μ.outerMeasure ↑U ≤ μ.outerMeasure A + ↑ε
• MeasureTheory.Content.outerMeasure_caratheodory 📋 Mathlib.MeasureTheory.Measure.Content
  {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] (A : Set G) : MeasurableSet A ↔ ∀ (U : TopologicalSpace.Opens G), μ.outerMeasure (↑U ∩ A) + μ.outerMeasure (↑U \ A) ≤ μ.outerMeasure ↑U
• MeasureTheory.Content.outerMeasure_exists_compact 📋 Mathlib.MeasureTheory.Measure.Content
  {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] {U : TopologicalSpace.Opens G} (hU : μ.outerMeasure ↑U ≠ ⊤) {ε : NNReal} (hε : ε ≠ 0) : ∃ K, ↑K ⊆ ↑U ∧ μ.outerMeasure ↑U ≤ μ.outerMeasure ↑K + ↑ε
• MeasureTheory.Content.outerMeasure_preimage 📋 Mathlib.MeasureTheory.Measure.Content
  {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] (f : G ≃ₜ G) (h : ∀ ⦃K : TopologicalSpace.Compacts G⦄, μ (TopologicalSpace.Compacts.map ⇑f ⋯ K) = μ K) (A : Set G) : μ.outerMeasure (⇑f ⁻¹' A) = μ.outerMeasure A
• MeasureTheory.Content.is_add_left_invariant_outerMeasure 📋 Mathlib.MeasureTheory.Measure.Content
  {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] [AddGroup G] [SeparatelyContinuousAdd G] (h : ∀ (g : G) {K : TopologicalSpace.Compacts G}, μ (TopologicalSpace.Compacts.map (fun x => g + x) ⋯ K) = μ K) (g : G) (A : Set G) : μ.outerMeasure ((fun x => g + x) ⁻¹' A) = μ.outerMeasure A
• MeasureTheory.Content.is_mul_left_invariant_outerMeasure 📋 Mathlib.MeasureTheory.Measure.Content
  {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] [Group G] [SeparatelyContinuousMul G] (h : ∀ (g : G) {K : TopologicalSpace.Compacts G}, μ (TopologicalSpace.Compacts.map (fun x => g * x) ⋯ K) = μ K) (g : G) (A : Set G) : μ.outerMeasure ((fun x => g * x) ⁻¹' A) = μ.outerMeasure A
• MeasureTheory.Content.outerMeasure_pos_of_is_add_left_invariant 📋 Mathlib.MeasureTheory.Measure.Content
  {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] [AddGroup G] [IsTopologicalAddGroup G] (h3 : ∀ (g : G) {K : TopologicalSpace.Compacts G}, μ (TopologicalSpace.Compacts.map (fun x => g + x) ⋯ K) = μ K) (K : TopologicalSpace.Compacts G) (hK : μ K ≠ 0) {U : Set G} (h1U : IsOpen U) (h2U : U.Nonempty) : 0 < μ.outerMeasure U
• MeasureTheory.Content.outerMeasure_pos_of_is_mul_left_invariant 📋 Mathlib.MeasureTheory.Measure.Content
  {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] [Group G] [IsTopologicalGroup G] (h3 : ∀ (g : G) {K : TopologicalSpace.Compacts G}, μ (TopologicalSpace.Compacts.map (fun x => g * x) ⋯ K) = μ K) (K : TopologicalSpace.Compacts G) (hK : μ K ≠ 0) {U : Set G} (h1U : IsOpen U) (h2U : U.Nonempty) : 0 < μ.outerMeasure U
• ContinuousMapZero.instR1Space 📋 Mathlib.Topology.ContinuousMap.ContinuousMapZero
  {X : Type u_1} {R : Type u_3} [Zero X] [Zero R] [TopologicalSpace X] [TopologicalSpace R] [R1Space R] : R1Space (ContinuousMapZero X R)
• exists_tsupport_one_of_isOpen_isClosed 📋 Mathlib.Topology.UrysohnsLemma
  {X : Type u_1} [TopologicalSpace X] [R1Space X] {s t : Set X} (hs : IsOpen s) (hscp : IsCompact (closure s)) (ht : IsClosed t) (hst : t ⊆ s) : ∃ f, tsupport ⇑f ⊆ s ∧ Set.EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Set.Icc 0 1
• exists_continuousMap_one_of_isCompact_subset_isOpen 📋 Mathlib.Topology.UrysohnsLemma
  {X : Type u_1} [TopologicalSpace X] [R1Space X] [LocallyCompactSpace X] {K V : Set X} (hK : IsCompact K) (hV : IsOpen V) (hKV : K ⊆ V) : ∃ f, Set.EqOn (⇑f) 1 K ∧ IsCompact (tsupport ⇑f) ∧ tsupport ⇑f ⊆ V ∧ ∀ (x : X), f x ∈ Set.Icc 0 1
• NormalSpace.of_paracompactSpace_r1Space 📋 Mathlib.Topology.Compactness.Paracompact
  {X : Type v} [TopologicalSpace X] [R1Space X] [ParacompactSpace X] : NormalSpace X
• MeasureTheory.ae_eq_zero_of_forall_setIntegral_isCompact_eq_zero 📋 Mathlib.MeasureTheory.Function.AEEqOfIntegral
  {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {β : Type u_3} [TopologicalSpace β] [MeasurableSpace β] [BorelSpace β] [SigmaCompactSpace β] [R1Space β] {μ : MeasureTheory.Measure β} {f : β → E} (hf : MeasureTheory.Integrable f μ) (h'f : ∀ (s : Set β), IsCompact s → ∫ (x : β) in s, f x ∂μ = 0) : f =ᵐ[μ] 0
• MeasureTheory.ae_eq_zero_of_forall_setIntegral_isCompact_eq_zero' 📋 Mathlib.MeasureTheory.Function.AEEqOfIntegral
  {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {β : Type u_3} [TopologicalSpace β] [MeasurableSpace β] [BorelSpace β] [SigmaCompactSpace β] [R1Space β] {μ : MeasureTheory.Measure β} {f : β → E} (hf : MeasureTheory.LocallyIntegrable f μ) (h'f : ∀ (s : Set β), IsCompact s → ∫ (x : β) in s, f x ∂μ = 0) : f =ᵐ[μ] 0
• OnePoint.instNormalSpaceOfWeaklyLocallyCompactSpaceOfR1Space 📋 Mathlib.Topology.Compactification.OnePoint.Basic
  {X : Type u_1} [TopologicalSpace X] [WeaklyLocallyCompactSpace X] [R1Space X] : NormalSpace (OnePoint X)
• MeasureTheory.Integrable.exists_hasCompactSupport_integral_sub_le 📋 Mathlib.MeasureTheory.Function.ContinuousMapDense
  {α : Type u_1} [TopologicalSpace α] [NormalSpace α] [MeasurableSpace α] [BorelSpace α] {E : Type u_2} [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} [NormedSpace ℝ E] [R1Space α] [WeaklyLocallyCompactSpace α] [μ.Regular] {f : α → E} (hf : MeasureTheory.Integrable f μ) {ε : ℝ} (hε : 0 < ε) : ∃ g, HasCompactSupport g ∧ ∫ (x : α), ‖f x - g x‖ ∂μ ≤ ε ∧ Continuous g ∧ MeasureTheory.Integrable g μ
• MeasureTheory.Integrable.exists_hasCompactSupport_lintegral_sub_le 📋 Mathlib.MeasureTheory.Function.ContinuousMapDense
  {α : Type u_1} [TopologicalSpace α] [NormalSpace α] [MeasurableSpace α] [BorelSpace α] {E : Type u_2} [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} [NormedSpace ℝ E] [R1Space α] [WeaklyLocallyCompactSpace α] [μ.Regular] {f : α → E} (hf : MeasureTheory.Integrable f μ) {ε : ENNReal} (hε : ε ≠ 0) : ∃ g, HasCompactSupport g ∧ ∫⁻ (x : α), ‖f x - g x‖ₑ ∂μ ≤ ε ∧ Continuous g ∧ MeasureTheory.Integrable g μ
• MeasureTheory.MemLp.exists_hasCompactSupport_integral_rpow_sub_le 📋 Mathlib.MeasureTheory.Function.ContinuousMapDense
  {α : Type u_1} [TopologicalSpace α] [NormalSpace α] [MeasurableSpace α] [BorelSpace α] {E : Type u_2} [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} [NormedSpace ℝ E] [R1Space α] [WeaklyLocallyCompactSpace α] [μ.Regular] {p : ℝ} (hp : 0 < p) {f : α → E} (hf : MeasureTheory.MemLp f (ENNReal.ofReal p) μ) {ε : ℝ} (hε : 0 < ε) : ∃ g, HasCompactSupport g ∧ ∫ (x : α), ‖f x - g x‖ ^ p ∂μ ≤ ε ∧ Continuous g ∧ MeasureTheory.MemLp g (ENNReal.ofReal p) μ
• MeasureTheory.MemLp.exists_hasCompactSupport_eLpNorm_sub_le 📋 Mathlib.MeasureTheory.Function.ContinuousMapDense
  {α : Type u_1} [TopologicalSpace α] [NormalSpace α] [MeasurableSpace α] [BorelSpace α] {E : Type u_2} [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [NormedSpace ℝ E] [R1Space α] [WeaklyLocallyCompactSpace α] [μ.Regular] (hp : p ≠ ⊤) {f : α → E} (hf : MeasureTheory.MemLp f p μ) {ε : ENNReal} (hε : ε ≠ 0) : ∃ g, HasCompactSupport g ∧ MeasureTheory.eLpNorm (f - g) p μ ≤ ε ∧ Continuous g ∧ MeasureTheory.MemLp g p μ
• MeasureTheory.innerRegularWRT_isCompact_isClosed_iff 📋 Mathlib.MeasureTheory.Measure.RegularityCompacts
  {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [R1Space α] : μ.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) IsClosed ↔ μ.InnerRegularWRT IsCompact IsClosed
• MeasureTheory.innerRegularWRT_isCompact_closure_iff 📋 Mathlib.MeasureTheory.Measure.RegularityCompacts
  {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [R1Space α] : μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed ↔ μ.InnerRegularWRT IsCompact IsClosed
• MeasureTheory.innerRegularWRT_isCompact_isClosed_iff_innerRegularWRT_isCompact_closure 📋 Mathlib.MeasureTheory.Measure.RegularityCompacts
  {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [R1Space α] : μ.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) IsClosed ↔ μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed
• MeasureTheory.isClosed_setOfPred_preimage_ae_eq 📋 Mathlib.MeasureTheory.Measure.ContinuousPreimage
  {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] [R1Space X] [TopologicalSpace Y] [MeasurableSpace Y] [BorelSpace Y] [R1Space Y] [TopologicalSpace Z] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [μ.InnerRegularCompactLTTop] [MeasureTheory.IsLocallyFiniteMeasure ν] {f : Z → C(X, Y)} (hf : Continuous f) (hfm : ∀ (z : Z), MeasureTheory.MeasurePreserving (⇑(f z)) μ ν) (s : Set X) {t : Set Y} (htm : MeasureTheory.NullMeasurableSet t ν) (ht : ν t ≠ ⊤) : IsClosed {z | ⇑(f z) ⁻¹' t =ᵐ[μ] s}
• MeasureTheory.isClosed_setOf_preimage_ae_eq 📋 Mathlib.MeasureTheory.Measure.ContinuousPreimage
  {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] [R1Space X] [TopologicalSpace Y] [MeasurableSpace Y] [BorelSpace Y] [R1Space Y] [TopologicalSpace Z] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [μ.InnerRegularCompactLTTop] [MeasureTheory.IsLocallyFiniteMeasure ν] {f : Z → C(X, Y)} (hf : Continuous f) (hfm : ∀ (z : Z), MeasureTheory.MeasurePreserving (⇑(f z)) μ ν) (s : Set X) {t : Set Y} (htm : MeasureTheory.NullMeasurableSet t ν) (ht : ν t ≠ ⊤) : IsClosed {z | ⇑(f z) ⁻¹' t =ᵐ[μ] s}
• MeasureTheory.tendsto_measure_symmDiff_preimage_nhds_zero 📋 Mathlib.MeasureTheory.Measure.ContinuousPreimage
  {α : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] [R1Space X] [TopologicalSpace Y] [MeasurableSpace Y] [BorelSpace Y] [R1Space Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [μ.InnerRegularCompactLTTop] [MeasureTheory.IsLocallyFiniteMeasure ν] {l : Filter α} {f : α → C(X, Y)} {g : C(X, Y)} {s : Set Y} (hfg : Filter.Tendsto f l (nhds g)) (hf : ∀ᶠ (a : α) in l, MeasureTheory.MeasurePreserving (⇑(f a)) μ ν) (hg : MeasureTheory.MeasurePreserving (⇑g) μ ν) (hs : MeasureTheory.NullMeasurableSet s ν) (hνs : ν s ≠ ⊤) : Filter.Tendsto (fun a => μ (symmDiff (⇑(f a) ⁻¹' s) (⇑g ⁻¹' s))) l (nhds 0)
• aeconst_of_dense_setOfPred_preimage_smul_eq 📋 Mathlib.Dynamics.Ergodic.Action.OfMinimal
  {M : Type u_1} [TopologicalSpace M] {X : Type u_2} [TopologicalSpace X] [R1Space X] [MeasurableSpace X] [BorelSpace X] [SMul M X] [ContinuousSMul M X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [ErgodicSMul M X μ] {s : Set X} (hsm : MeasureTheory.NullMeasurableSet s μ) (hd : Dense {g | (fun x => g • x) ⁻¹' s = s}) : Filter.EventuallyConst s (MeasureTheory.ae μ)
• aeconst_of_dense_setOfPred_preimage_vadd_eq 📋 Mathlib.Dynamics.Ergodic.Action.OfMinimal
  {M : Type u_1} [TopologicalSpace M] {X : Type u_2} [TopologicalSpace X] [R1Space X] [MeasurableSpace X] [BorelSpace X] [VAdd M X] [ContinuousVAdd M X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [ErgodicVAdd M X μ] {s : Set X} (hsm : MeasureTheory.NullMeasurableSet s μ) (hd : Dense {g | (fun x => g +ᵥ x) ⁻¹' s = s}) : Filter.EventuallyConst s (MeasureTheory.ae μ)
• aeconst_of_dense_setOf_preimage_smul_eq 📋 Mathlib.Dynamics.Ergodic.Action.OfMinimal
  {M : Type u_1} [TopologicalSpace M] {X : Type u_2} [TopologicalSpace X] [R1Space X] [MeasurableSpace X] [BorelSpace X] [SMul M X] [ContinuousSMul M X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [ErgodicSMul M X μ] {s : Set X} (hsm : MeasureTheory.NullMeasurableSet s μ) (hd : Dense {g | (fun x => g • x) ⁻¹' s = s}) : Filter.EventuallyConst s (MeasureTheory.ae μ)
• aeconst_of_dense_setOf_preimage_vadd_eq 📋 Mathlib.Dynamics.Ergodic.Action.OfMinimal
  {M : Type u_1} [TopologicalSpace M] {X : Type u_2} [TopologicalSpace X] [R1Space X] [MeasurableSpace X] [BorelSpace X] [VAdd M X] [ContinuousVAdd M X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [ErgodicVAdd M X μ] {s : Set X} (hsm : MeasureTheory.NullMeasurableSet s μ) (hd : Dense {g | (fun x => g +ᵥ x) ⁻¹' s = s}) : Filter.EventuallyConst s (MeasureTheory.ae μ)
• aeconst_of_dense_setOfPred_preimage_smul_ae 📋 Mathlib.Dynamics.Ergodic.Action.OfMinimal
  {M : Type u_1} [TopologicalSpace M] {X : Type u_2} [TopologicalSpace X] [R1Space X] [MeasurableSpace X] [BorelSpace X] [SMul M X] [ContinuousSMul M X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [ErgodicSMul M X μ] {s : Set X} (hsm : MeasureTheory.NullMeasurableSet s μ) (hd : Dense {g | (fun x => g • x) ⁻¹' s =ᵐ[μ] s}) : Filter.EventuallyConst s (MeasureTheory.ae μ)
• aeconst_of_dense_setOfPred_preimage_vadd_ae 📋 Mathlib.Dynamics.Ergodic.Action.OfMinimal
  {M : Type u_1} [TopologicalSpace M] {X : Type u_2} [TopologicalSpace X] [R1Space X] [MeasurableSpace X] [BorelSpace X] [VAdd M X] [ContinuousVAdd M X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [ErgodicVAdd M X μ] {s : Set X} (hsm : MeasureTheory.NullMeasurableSet s μ) (hd : Dense {g | (fun x => g +ᵥ x) ⁻¹' s =ᵐ[μ] s}) : Filter.EventuallyConst s (MeasureTheory.ae μ)
• aeconst_of_dense_setOf_preimage_smul_ae 📋 Mathlib.Dynamics.Ergodic.Action.OfMinimal
  {M : Type u_1} [TopologicalSpace M] {X : Type u_2} [TopologicalSpace X] [R1Space X] [MeasurableSpace X] [BorelSpace X] [SMul M X] [ContinuousSMul M X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [ErgodicSMul M X μ] {s : Set X} (hsm : MeasureTheory.NullMeasurableSet s μ) (hd : Dense {g | (fun x => g • x) ⁻¹' s =ᵐ[μ] s}) : Filter.EventuallyConst s (MeasureTheory.ae μ)
• aeconst_of_dense_setOf_preimage_vadd_ae 📋 Mathlib.Dynamics.Ergodic.Action.OfMinimal
  {M : Type u_1} [TopologicalSpace M] {X : Type u_2} [TopologicalSpace X] [R1Space X] [MeasurableSpace X] [BorelSpace X] [VAdd M X] [ContinuousVAdd M X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [ErgodicVAdd M X μ] {s : Set X} (hsm : MeasureTheory.NullMeasurableSet s μ) (hd : Dense {g | (fun x => g +ᵥ x) ⁻¹' s =ᵐ[μ] s}) : Filter.EventuallyConst s (MeasureTheory.ae μ)
• ergodic_smul_of_denseRange_pow 📋 Mathlib.Dynamics.Ergodic.Action.OfMinimal
  {X : Type u_2} [TopologicalSpace X] [R1Space X] [MeasurableSpace X] [BorelSpace X] {M : Type u_3} [Monoid M] [TopologicalSpace M] [MulAction M X] [ContinuousSMul M X] {g : M} (hg : DenseRange fun x => g ^ x) (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [ErgodicSMul M X μ] : Ergodic (fun x => g • x) μ
• ergodic_vadd_of_denseRange_nsmul 📋 Mathlib.Dynamics.Ergodic.Action.OfMinimal
  {X : Type u_2} [TopologicalSpace X] [R1Space X] [MeasurableSpace X] [BorelSpace X] {M : Type u_3} [AddMonoid M] [TopologicalSpace M] [AddAction M X] [ContinuousVAdd M X] {g : M} (hg : DenseRange fun x => x • g) (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [ErgodicVAdd M X μ] : Ergodic (fun x => g +ᵥ x) μ
• ErgodicSMul.trans_isMinimal 📋 Mathlib.Dynamics.Ergodic.Action.OfMinimal
  {M : Type u_1} {X : Type u_2} [Monoid M] [SMul M X] [TopologicalSpace X] [R1Space X] [MeasurableSpace X] [BorelSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] (N : Type u_3) [MulAction M N] [Monoid N] [TopologicalSpace N] [MulAction.IsMinimal M N] [MulAction N X] [IsScalarTower M N X] [ContinuousSMul N X] [ErgodicSMul N X μ] : ErgodicSMul M X μ
• ErgodicVAdd.trans_isMinimal 📋 Mathlib.Dynamics.Ergodic.Action.OfMinimal
  {M : Type u_1} {X : Type u_2} [AddMonoid M] [VAdd M X] [TopologicalSpace X] [R1Space X] [MeasurableSpace X] [BorelSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] (N : Type u_3) [AddAction M N] [AddMonoid N] [TopologicalSpace N] [AddAction.IsMinimal M N] [AddAction N X] [VAddAssocClass M N X] [ContinuousVAdd N X] [ErgodicVAdd N X μ] : ErgodicVAdd M X μ
• ergodic_smul_of_denseRange_zpow 📋 Mathlib.Dynamics.Ergodic.Action.OfMinimal
  {G : Type u_1} [Group G] [TopologicalSpace G] [ContinuousInv G] {X : Type u_2} [TopologicalSpace X] [R1Space X] [MeasurableSpace X] [BorelSpace X] [MulAction G X] [ContinuousSMul G X] {g : G} (hg : DenseRange fun x => g ^ x) (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [ErgodicSMul G X μ] : Ergodic (fun x => g • x) μ
• ergodic_vadd_of_denseRange_zsmul 📋 Mathlib.Dynamics.Ergodic.Action.OfMinimal
  {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ContinuousNeg G] {X : Type u_2} [TopologicalSpace X] [R1Space X] [MeasurableSpace X] [BorelSpace X] [AddAction G X] [ContinuousVAdd G X] {g : G} (hg : DenseRange fun x => x • g) (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [ErgodicVAdd G X μ] : Ergodic (fun x => g +ᵥ x) μ
• aeconst_of_dense_aestabilizer_smul 📋 Mathlib.Dynamics.Ergodic.Action.OfMinimal
  {G : Type u_1} [Group G] [TopologicalSpace G] [ContinuousInv G] {X : Type u_2} [TopologicalSpace X] [R1Space X] [MeasurableSpace X] [BorelSpace X] [MulAction G X] [ContinuousSMul G X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [ErgodicSMul G X μ] {s : Set X} (hsm : MeasureTheory.NullMeasurableSet s μ) (hd : Dense ↑(MulAction.aestabilizer G μ s)) : Filter.EventuallyConst s (MeasureTheory.ae μ)
• aeconst_of_dense_aestabilizer_vadd 📋 Mathlib.Dynamics.Ergodic.Action.OfMinimal
  {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ContinuousNeg G] {X : Type u_2} [TopologicalSpace X] [R1Space X] [MeasurableSpace X] [BorelSpace X] [AddAction G X] [ContinuousVAdd G X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [ErgodicVAdd G X μ] {s : Set X} (hsm : MeasureTheory.NullMeasurableSet s μ) (hd : Dense ↑(AddAction.aestabilizer G μ s)) : Filter.EventuallyConst s (MeasureTheory.ae μ)
• Function.HasCompactFixedSupport_iff 📋 Mathlib.Dynamics.FixedPoints.Support
  {X : Type u_1} [TopologicalSpace X] {f : X → X} [R1Space X] : Function.HasCompactFixedSupport f ↔ ∃ K, IsCompact K ∧ (Function.fixedPoints f)ᶜ ⊆ K
• uniformSpaceOfCompactR1 📋 Mathlib.Topology.UniformSpace.OfCompactT2
  {γ : Type u_1} [TopologicalSpace γ] [CompactSpace γ] [R1Space γ] : UniformSpace γ
• MeasureTheory.FiniteMeasure.instR1Space 📋 Mathlib.MeasureTheory.Measure.FiniteMeasure
  {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] : R1Space (MeasureTheory.FiniteMeasure Ω)
• MeasureTheory.ProbabilityMeasure.R1Space 📋 Mathlib.MeasureTheory.Measure.ProbabilityMeasure
  {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] : R1Space (MeasureTheory.ProbabilityMeasure Ω)
• Continuous.compMeasurePreservingLp 📋 Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] [R1Space X] [TopologicalSpace Y] [MeasurableSpace Y] [BorelSpace Y] [R1Space Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [μ.InnerRegularCompactLTTop] [MeasureTheory.IsLocallyFiniteMeasure ν] {E : Type u_3} [NormedAddCommGroup E] {p : ENNReal} [Fact (1 ≤ p)] {Z : Type u_4} [TopologicalSpace Z] {f : Z → ↥(MeasureTheory.Lp E p ν)} {g : Z → C(X, Y)} (hf : Continuous f) (hg : Continuous g) (hgm : ∀ (z : Z), MeasureTheory.MeasurePreserving (⇑(g z)) μ ν) (hp : p ≠ ⊤) : Continuous fun z => (MeasureTheory.Lp.compMeasurePreserving ⇑(g z) ⋯) (f z)
• ContinuousAt.compMeasurePreservingLp 📋 Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] [R1Space X] [TopologicalSpace Y] [MeasurableSpace Y] [BorelSpace Y] [R1Space Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [μ.InnerRegularCompactLTTop] [MeasureTheory.IsLocallyFiniteMeasure ν] {E : Type u_3} [NormedAddCommGroup E] {p : ENNReal} [Fact (1 ≤ p)] {Z : Type u_4} [TopologicalSpace Z] {f : Z → ↥(MeasureTheory.Lp E p ν)} {g : Z → C(X, Y)} {z : Z} (hf : ContinuousAt f z) (hg : ContinuousAt g z) (hgm : ∀ (z : Z), MeasureTheory.MeasurePreserving (⇑(g z)) μ ν) (hp : p ≠ ⊤) : ContinuousAt (fun z => (MeasureTheory.Lp.compMeasurePreserving ⇑(g z) ⋯) (f z)) z
• ContinuousOn.compMeasurePreservingLp 📋 Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] [R1Space X] [TopologicalSpace Y] [MeasurableSpace Y] [BorelSpace Y] [R1Space Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [μ.InnerRegularCompactLTTop] [MeasureTheory.IsLocallyFiniteMeasure ν] {E : Type u_3} [NormedAddCommGroup E] {p : ENNReal} [Fact (1 ≤ p)] {Z : Type u_4} [TopologicalSpace Z] {f : Z → ↥(MeasureTheory.Lp E p ν)} {g : Z → C(X, Y)} {s : Set Z} (hf : ContinuousOn f s) (hg : ContinuousOn g s) (hgm : ∀ (z : Z), MeasureTheory.MeasurePreserving (⇑(g z)) μ ν) (hp : p ≠ ⊤) : ContinuousOn (fun z => (MeasureTheory.Lp.compMeasurePreserving ⇑(g z) ⋯) (f z)) s
• ContinuousWithinAt.compMeasurePreservingLp 📋 Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] [R1Space X] [TopologicalSpace Y] [MeasurableSpace Y] [BorelSpace Y] [R1Space Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [μ.InnerRegularCompactLTTop] [MeasureTheory.IsLocallyFiniteMeasure ν] {E : Type u_3} [NormedAddCommGroup E] {p : ENNReal} [Fact (1 ≤ p)] {Z : Type u_4} [TopologicalSpace Z] {f : Z → ↥(MeasureTheory.Lp E p ν)} {g : Z → C(X, Y)} {s : Set Z} {z : Z} (hf : ContinuousWithinAt f s z) (hg : ContinuousWithinAt g s z) (hgm : ∀ (z : Z), MeasureTheory.MeasurePreserving (⇑(g z)) μ ν) (hp : p ≠ ⊤) : ContinuousWithinAt (fun z => (MeasureTheory.Lp.compMeasurePreserving ⇑(g z) ⋯) (f z)) s z
• MeasureTheory.Lp.compMeasurePreserving_continuous 📋 Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] [R1Space X] [TopologicalSpace Y] [MeasurableSpace Y] [BorelSpace Y] [R1Space Y] (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) [μ.InnerRegularCompactLTTop] [MeasureTheory.IsLocallyFiniteMeasure ν] (E : Type u_3) [NormedAddCommGroup E] {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) : Continuous fun gf => (MeasureTheory.Lp.compMeasurePreserving ⇑↑gf.2 ⋯) gf.1
• Filter.Tendsto.compMeasurePreservingLp 📋 Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] [R1Space X] [TopologicalSpace Y] [MeasurableSpace Y] [BorelSpace Y] [R1Space Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [μ.InnerRegularCompactLTTop] [MeasureTheory.IsLocallyFiniteMeasure ν] {E : Type u_3} [NormedAddCommGroup E] {p : ENNReal} [Fact (1 ≤ p)] {α : Type u_4} {l : Filter α} {f : α → ↥(MeasureTheory.Lp E p ν)} {f₀ : ↥(MeasureTheory.Lp E p ν)} {g : α → C(X, Y)} {g₀ : C(X, Y)} (hf : Filter.Tendsto f l (nhds f₀)) (hg : Filter.Tendsto g l (nhds g₀)) (hgm : ∀ (a : α), MeasureTheory.MeasurePreserving (⇑(g a)) μ ν) (hgm₀ : MeasureTheory.MeasurePreserving (⇑g₀) μ ν) (hp : p ≠ ⊤) : Filter.Tendsto (fun a => (MeasureTheory.Lp.compMeasurePreserving ⇑(g a) ⋯) (f a)) l (nhds ((MeasureTheory.Lp.compMeasurePreserving (⇑g₀) hgm₀) f₀))
• DomAddAct.instR1Space 📋 Mathlib.Topology.Algebra.Constructions.DomMulAct
  {M : Type u_1} [TopologicalSpace M] [R1Space M] : R1Space Mᵈᵃᵃ
• DomMulAct.instR1Space 📋 Mathlib.Topology.Algebra.Constructions.DomMulAct
  {M : Type u_1} [TopologicalSpace M] [R1Space M] : R1Space Mᵈᵐᵃ
• MeasureTheory.Lp.instContinuousSMulDomMulAct 📋 Mathlib.MeasureTheory.Function.LpSpace.DomAct.Continuous
  {X : Type u_1} {M : Type u_2} {E : Type u_3} [TopologicalSpace X] [R1Space X] [MeasurableSpace X] [BorelSpace X] [TopologicalSpace M] [MeasurableSpace M] [OpensMeasurableSpace M] [SMul M X] [ContinuousSMul M X] [NormedAddCommGroup E] {μ : MeasureTheory.Measure X} [MeasureTheory.IsLocallyFiniteMeasure μ] [μ.InnerRegularCompactLTTop] [MeasureTheory.SMulInvariantMeasure M X μ] {p : ENNReal} [Fact (1 ≤ p)] [hp : Fact (p ≠ ⊤)] : ContinuousSMul Mᵈᵐᵃ ↥(MeasureTheory.Lp E p μ)
• MeasureTheory.Lp.instContinuousVAddDomAddAct 📋 Mathlib.MeasureTheory.Function.LpSpace.DomAct.Continuous
  {X : Type u_1} {M : Type u_2} {E : Type u_3} [TopologicalSpace X] [R1Space X] [MeasurableSpace X] [BorelSpace X] [TopologicalSpace M] [MeasurableSpace M] [OpensMeasurableSpace M] [VAdd M X] [ContinuousVAdd M X] [NormedAddCommGroup E] {μ : MeasureTheory.Measure X} [MeasureTheory.IsLocallyFiniteMeasure μ] [μ.InnerRegularCompactLTTop] [MeasureTheory.VAddInvariantMeasure M X μ] {p : ENNReal} [Fact (1 ≤ p)] [hp : Fact (p ≠ ⊤)] : ContinuousVAdd Mᵈᵃᵃ ↥(MeasureTheory.Lp E p μ)
• CompactlySupportedContinuousMap.pullback_addMonoidHom 📋 Mathlib.Topology.ContinuousMap.CompactlySupported
  {α : Type u_2} {β : Type u_3} {γ : Type u_4} [TopologicalSpace α] [R1Space α] [AddGroup α] [TopologicalSpace β] [R1Space β] [AddGroup β] [ContinuousAdd β] [NormedAddCommGroup γ] {φ : α →+ β} (hφ : Topology.IsClosedEmbedding ⇑φ) (f : CompactlySupportedContinuousMap β γ) (b : β) : CompactlySupportedContinuousMap α γ
• CompactlySupportedContinuousMap.pullback_monoidHom 📋 Mathlib.Topology.ContinuousMap.CompactlySupported
  {α : Type u_2} {β : Type u_3} {γ : Type u_4} [TopologicalSpace α] [R1Space α] [Group α] [TopologicalSpace β] [R1Space β] [Group β] [ContinuousMul β] [NormedAddCommGroup γ] {φ : α →* β} (hφ : Topology.IsClosedEmbedding ⇑φ) (f : CompactlySupportedContinuousMap β γ) (b : β) : CompactlySupportedContinuousMap α γ
• CompactlySupportedContinuousMap.pullback_addMonoidHom_def 📋 Mathlib.Topology.ContinuousMap.CompactlySupported
  {α : Type u_2} {β : Type u_3} {γ : Type u_4} [TopologicalSpace α] [R1Space α] [AddGroup α] [TopologicalSpace β] [R1Space β] [AddGroup β] [ContinuousAdd β] [NormedAddCommGroup γ] {φ : α →+ β} (hφ : Topology.IsClosedEmbedding ⇑φ) (f : CompactlySupportedContinuousMap β γ) (b : β) (a : α) : (CompactlySupportedContinuousMap.pullback_addMonoidHom hφ f b) a = f (b + φ a)
• CompactlySupportedContinuousMap.pullback_monoidHom_def 📋 Mathlib.Topology.ContinuousMap.CompactlySupported
  {α : Type u_2} {β : Type u_3} {γ : Type u_4} [TopologicalSpace α] [R1Space α] [Group α] [TopologicalSpace β] [R1Space β] [Group β] [ContinuousMul β] [NormedAddCommGroup γ] {φ : α →* β} (hφ : Topology.IsClosedEmbedding ⇑φ) (f : CompactlySupportedContinuousMap β γ) (b : β) (a : α) : (CompactlySupportedContinuousMap.pullback_monoidHom hφ f b) a = f (b * φ a)
• BaireSpace.of_t2Space_locallyCompactSpace 📋 Mathlib.Topology.Baire.LocallyCompactRegular
  {X : Type u_1} [TopologicalSpace X] [R1Space X] [LocallyCompactSpace X] : BaireSpace X
• IsGδ.baireSpace_of_t2Space_locallyCompactSpace 📋 Mathlib.Topology.Baire.LocallyCompactRegular
  {X : Type u_1} [TopologicalSpace X] {s : Set X} [R1Space X] [LocallyCompactSpace X] (hG : IsGδ s) : BaireSpace ↑s
• IsGδ.of_t2Space_locallyCompactSpace 📋 Mathlib.Topology.Baire.LocallyCompactRegular
  {X : Type u_1} [TopologicalSpace X] {s : Set X} [R1Space X] [LocallyCompactSpace X] (hG : IsGδ s) : BaireSpace ↑s
• ZeroAtInftyContinuousMap.toOnePoint 📋 Mathlib.Topology.ContinuousMap.ZeroAtInftyUnitization
  {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [Zero R] (f : ZeroAtInftyContinuousMap X R) : C(OnePoint X, R)
• ZeroAtInftyContinuousMap.toOnePoint_injective 📋 Mathlib.Topology.ContinuousMap.ZeroAtInftyUnitization
  {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [Zero R] : Function.Injective ZeroAtInftyContinuousMap.toOnePoint
• ContinuousMap.toZeroAtInfty 📋 Mathlib.Topology.ContinuousMap.ZeroAtInftyUnitization
  {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] (g : C(OnePoint X, R)) : ZeroAtInftyContinuousMap X R
• ZeroAtInftyContinuousMap.unitizationEquiv 📋 Mathlib.Topology.ContinuousMap.ZeroAtInftyUnitization
  (X : Type u_1) (R : Type u_2) [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] : Unitization R (ZeroAtInftyContinuousMap X R) ≃ C(OnePoint X, R)
• ZeroAtInftyContinuousMap.toOnePointNonUnitalRingHom 📋 Mathlib.Topology.ContinuousMap.ZeroAtInftyUnitization
  (X : Type u_1) (R : Type u_2) [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [NonUnitalNonAssocSemiring R] [IsTopologicalSemiring R] : ZeroAtInftyContinuousMap X R →ₙ+* C(OnePoint X, R)
• ZeroAtInftyContinuousMap.toOnePoint_infty 📋 Mathlib.Topology.ContinuousMap.ZeroAtInftyUnitization
  {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [Zero R] (f : ZeroAtInftyContinuousMap X R) : f.toOnePoint OnePoint.infty = 0
• ZeroAtInftyContinuousMap.toOnePoint_coe 📋 Mathlib.Topology.ContinuousMap.ZeroAtInftyUnitization
  {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [Zero R] (f : ZeroAtInftyContinuousMap X R) (x : X) : f.toOnePoint ↑x = f x
• ZeroAtInftyContinuousMap.toOnePoint_zero 📋 Mathlib.Topology.ContinuousMap.ZeroAtInftyUnitization
  {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [Zero R] : ZeroAtInftyContinuousMap.toOnePoint 0 = 0
• ZeroAtInftyContinuousMap.toOnePointAddMonoidHom 📋 Mathlib.Topology.ContinuousMap.ZeroAtInftyUnitization
  (X : Type u_1) (R : Type u_2) [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddMonoid R] [ContinuousAdd R] : ZeroAtInftyContinuousMap X R →+ C(OnePoint X, R)
• ContinuousMap.toZeroAtInfty_const 📋 Mathlib.Topology.ContinuousMap.ZeroAtInftyUnitization
  {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] (r : R) : (ContinuousMap.const (OnePoint X) r).toZeroAtInfty = 0
• ContinuousMap.toZeroAtInftyAddMonoidHom 📋 Mathlib.Topology.ContinuousMap.ZeroAtInftyUnitization
  (X : Type u_1) (R : Type u_2) [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] : C(OnePoint X, R) →+ ZeroAtInftyContinuousMap X R
• ZeroAtInftyContinuousMap.unitizationAddEquiv 📋 Mathlib.Topology.ContinuousMap.ZeroAtInftyUnitization
  (X : Type u_1) (R : Type u_2) [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] : Unitization R (ZeroAtInftyContinuousMap X R) ≃+ C(OnePoint X, R)
• ZeroAtInftyContinuousMap.toOnePoint_star 📋 Mathlib.Topology.ContinuousMap.ZeroAtInftyUnitization
  {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddMonoid R] [StarAddMonoid R] [ContinuousStar R] (f : ZeroAtInftyContinuousMap X R) : (star f).toOnePoint = star f.toOnePoint
• ContinuousMap.toZeroAtInfty_neg 📋 Mathlib.Topology.ContinuousMap.ZeroAtInftyUnitization
  {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] (g : C(OnePoint X, R)) : (-g).toZeroAtInfty = -g.toZeroAtInfty
• ZeroAtInftyContinuousMap.toOnePoint_neg 📋 Mathlib.Topology.ContinuousMap.ZeroAtInftyUnitization
  {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddGroup R] [IsTopologicalAddGroup R] (f : ZeroAtInftyContinuousMap X R) : (-f).toOnePoint = -f.toOnePoint
• ContinuousMap.toZeroAtInfty_zero 📋 Mathlib.Topology.ContinuousMap.ZeroAtInftyUnitization
  {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] : ContinuousMap.toZeroAtInfty 0 = 0
• ContinuousMap.toZeroAtInfty_apply 📋 Mathlib.Topology.ContinuousMap.ZeroAtInftyUnitization
  {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] (g : C(OnePoint X, R)) (x : X) : g.toZeroAtInfty x = g ↑x - g OnePoint.infty
• ZeroAtInftyContinuousMap.toOnePointLinearMap 📋 Mathlib.Topology.ContinuousMap.ZeroAtInftyUnitization
  (X : Type u_1) (R : Type u_2) (S : Type u_3) [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [Semiring S] [AddCommMonoid R] [ContinuousAdd R] [Module S R] [ContinuousConstSMul S R] : ZeroAtInftyContinuousMap X R →ₗ[S] C(OnePoint X, R)
• ZeroAtInftyContinuousMap.toOnePoint_smul 📋 Mathlib.Topology.ContinuousMap.ZeroAtInftyUnitization
  {X : Type u_1} {R : Type u_2} {S : Type u_3} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [Zero R] [Zero S] [SMulWithZero S R] [ContinuousConstSMul S R] (s : S) (f : ZeroAtInftyContinuousMap X R) : (s • f).toOnePoint = s • f.toOnePoint
• ContinuousMap.toZeroAtInfty_star 📋 Mathlib.Topology.ContinuousMap.ZeroAtInftyUnitization
  {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] [StarAddMonoid R] [ContinuousStar R] (g : C(OnePoint X, R)) : (star g).toZeroAtInfty = star g.toZeroAtInfty
• ZeroAtInftyContinuousMap.toOnePointNonUnitalRingHom_apply 📋 Mathlib.Topology.ContinuousMap.ZeroAtInftyUnitization
  (X : Type u_1) (R : Type u_2) [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [NonUnitalNonAssocSemiring R] [IsTopologicalSemiring R] (f : ZeroAtInftyContinuousMap X R) : (ZeroAtInftyContinuousMap.toOnePointNonUnitalRingHom X R) f = f.toOnePoint
• ZeroAtInftyContinuousMap.toEquiv_unitizationAddEquiv 📋 Mathlib.Topology.ContinuousMap.ZeroAtInftyUnitization
  {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] : (ZeroAtInftyContinuousMap.unitizationAddEquiv X R).toEquiv = ZeroAtInftyContinuousMap.unitizationEquiv X R
• ZeroAtInftyContinuousMap.toOnePoint_mul 📋 Mathlib.Topology.ContinuousMap.ZeroAtInftyUnitization
  {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [MulZeroClass R] [ContinuousMul R] (f g : ZeroAtInftyContinuousMap X R) : (f * g).toOnePoint = f.toOnePoint * g.toOnePoint
• ZeroAtInftyContinuousMap.toOnePoint_add 📋 Mathlib.Topology.ContinuousMap.ZeroAtInftyUnitization
  {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddZeroClass R] [ContinuousAdd R] (f g : ZeroAtInftyContinuousMap X R) : (f + g).toOnePoint = f.toOnePoint + g.toOnePoint
• ContinuousMap.toZeroAtInftyLinearMap 📋 Mathlib.Topology.ContinuousMap.ZeroAtInftyUnitization
  (X : Type u_1) (R : Type u_2) (S : Type u_3) [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] [Semiring S] [Module S R] [ContinuousConstSMul S R] : C(OnePoint X, R) →ₗ[S] ZeroAtInftyContinuousMap X R
• ZeroAtInftyContinuousMap.toAddMonoidHom_toOnePointNonUnitalRingHom 📋 Mathlib.Topology.ContinuousMap.ZeroAtInftyUnitization
  (X : Type u_1) (R : Type u_2) [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [NonUnitalNonAssocSemiring R] [IsTopologicalSemiring R] : (ZeroAtInftyContinuousMap.toOnePointNonUnitalRingHom X R).toAddMonoidHom = ZeroAtInftyContinuousMap.toOnePointAddMonoidHom X R
• ZeroAtInftyContinuousMap.toOnePointNonUnitalAlgHom 📋 Mathlib.Topology.ContinuousMap.ZeroAtInftyUnitization
  (X : Type u_1) (R : Type u_2) (S : Type u_3) [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [NonUnitalNonAssocSemiring R] [IsTopologicalSemiring R] [Semiring S] [Module S R] [ContinuousConstSMul S R] : ZeroAtInftyContinuousMap X R →ₙₐ[S] C(OnePoint X, R)
• ContinuousMap.toZeroAtInfty_sub 📋 Mathlib.Topology.ContinuousMap.ZeroAtInftyUnitization
  {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] (g h : C(OnePoint X, R)) : (g - h).toZeroAtInfty = g.toZeroAtInfty - h.toZeroAtInfty
• ZeroAtInftyContinuousMap.toOnePoint_sub 📋 Mathlib.Topology.ContinuousMap.ZeroAtInftyUnitization
  {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddGroup R] [IsTopologicalAddGroup R] (f g : ZeroAtInftyContinuousMap X R) : (f - g).toOnePoint = f.toOnePoint - g.toOnePoint
• ContinuousMap.toZeroAtInfty_add 📋 Mathlib.Topology.ContinuousMap.ZeroAtInftyUnitization
  {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] (g h : C(OnePoint X, R)) : (g + h).toZeroAtInfty = g.toZeroAtInfty + h.toZeroAtInfty
• ZeroAtInftyContinuousMap.toOnePointAddMonoidHom_apply 📋 Mathlib.Topology.ContinuousMap.ZeroAtInftyUnitization
  (X : Type u_1) (R : Type u_2) [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddMonoid R] [ContinuousAdd R] (f : ZeroAtInftyContinuousMap X R) : (ZeroAtInftyContinuousMap.toOnePointAddMonoidHom X R) f = f.toOnePoint
• ZeroAtInftyContinuousMap.unitizationEquiv_inl 📋 Mathlib.Topology.ContinuousMap.ZeroAtInftyUnitization
  {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] (r : R) : (ZeroAtInftyContinuousMap.unitizationEquiv X R) (Unitization.inl r) = ContinuousMap.const (OnePoint X) r
• ZeroAtInftyContinuousMap.toOnePointNonUnitalStarAlgHom 📋 Mathlib.Topology.ContinuousMap.ZeroAtInftyUnitization
  (X : Type u_1) (R : Type u_2) (S : Type u_3) [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [NonUnitalNonAssocSemiring R] [IsTopologicalSemiring R] [Semiring S] [Module S R] [ContinuousConstSMul S R] [StarRing R] [ContinuousStar R] : ZeroAtInftyContinuousMap X R →⋆ₙₐ[S] C(OnePoint X, R)
• ZeroAtInftyContinuousMap.unitizationEquiv_inr 📋 Mathlib.Topology.ContinuousMap.ZeroAtInftyUnitization
  {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] (f : ZeroAtInftyContinuousMap X R) : (ZeroAtInftyContinuousMap.unitizationEquiv X R) ↑f = f.toOnePoint
• ZeroAtInftyContinuousMap.unitizationEquiv_apply_infty 📋 Mathlib.Topology.ContinuousMap.ZeroAtInftyUnitization
  {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] (f : Unitization R (ZeroAtInftyContinuousMap X R)) : ((ZeroAtInftyContinuousMap.unitizationEquiv X R) f) OnePoint.infty = f.toProd.1
• ZeroAtInftyContinuousMap.unitizationLinearEquiv 📋 Mathlib.Topology.ContinuousMap.ZeroAtInftyUnitization
  (X : Type u_1) (R : Type u_2) (S : Type u_3) [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] [Semiring S] [Module S R] [ContinuousConstSMul S R] : Unitization R (ZeroAtInftyContinuousMap X R) ≃ₗ[S] C(OnePoint X, R)
• ZeroAtInftyContinuousMap.toAddMonoidHom_toOnePointLinearMap 📋 Mathlib.Topology.ContinuousMap.ZeroAtInftyUnitization
  (X : Type u_1) (R : Type u_2) (S : Type u_3) [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [Semiring S] [AddCommMonoid R] [ContinuousAdd R] [Module S R] [ContinuousConstSMul S R] : (ZeroAtInftyContinuousMap.toOnePointLinearMap X R S).toAddMonoidHom = ZeroAtInftyContinuousMap.toOnePointAddMonoidHom X R
• ContinuousMap.toZeroAtInftyAddMonoidHom_apply 📋 Mathlib.Topology.ContinuousMap.ZeroAtInftyUnitization
  (X : Type u_1) (R : Type u_2) [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] (g : C(OnePoint X, R)) : (ContinuousMap.toZeroAtInftyAddMonoidHom X R) g = g.toZeroAtInfty
• ZeroAtInftyContinuousMap.unitizationEquiv_symm_apply 📋 Mathlib.Topology.ContinuousMap.ZeroAtInftyUnitization
  {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] (g : C(OnePoint X, R)) : (ZeroAtInftyContinuousMap.unitizationEquiv X R).symm g = Unitization.mk (g OnePoint.infty, g.toZeroAtInfty)
• ZeroAtInftyContinuousMap.toOnePointLinearMap_apply 📋 Mathlib.Topology.ContinuousMap.ZeroAtInftyUnitization
  (X : Type u_1) (R : Type u_2) (S : Type u_3) [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [Semiring S] [AddCommMonoid R] [ContinuousAdd R] [Module S R] [ContinuousConstSMul S R] (f : ZeroAtInftyContinuousMap X R) : (ZeroAtInftyContinuousMap.toOnePointLinearMap X R S) f = f.toOnePoint

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 ce5dd8c