Loogle!
Result
Found 304 definitions whose name contains "fundamental". Of these, only the first 200 are shown.
- Ordinal.IsFundamentalSequence Mathlib.SetTheory.Cardinal.Cofinality
Ordinal.{u} → (o : Ordinal.{u}) → ((b : Ordinal.{u}) → b < o → Ordinal.{u}) → Prop - Ordinal.IsFundamentalSequence.blsub_eq Mathlib.SetTheory.Cardinal.Cofinality
∀ {a o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{u}}, a.IsFundamentalSequence o f → o.blsub f = a - Ordinal.IsFundamentalSequence.cof_eq Mathlib.SetTheory.Cardinal.Cofinality
∀ {a o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{u}}, a.IsFundamentalSequence o f → a.cof.ord = o - Ordinal.IsFundamentalSequence.id_of_le_cof Mathlib.SetTheory.Cardinal.Cofinality
∀ {o : Ordinal.{u}}, o ≤ o.cof.ord → o.IsFundamentalSequence o fun a x => a - Ordinal.IsFundamentalSequence.zero Mathlib.SetTheory.Cardinal.Cofinality
∀ {f : (b : Ordinal.{u_2}) → b < 0 → Ordinal.{u_2}}, Ordinal.IsFundamentalSequence 0 0 f - Ordinal.IsFundamentalSequence.succ Mathlib.SetTheory.Cardinal.Cofinality
∀ {o : Ordinal.{u}}, (Order.succ o).IsFundamentalSequence 1 fun x x => o - Ordinal.exists_fundamental_sequence Mathlib.SetTheory.Cardinal.Cofinality
∀ (a : Ordinal.{u}), ∃ f, a.IsFundamentalSequence a.cof.ord f - Ordinal.IsNormal.isFundamentalSequence Mathlib.SetTheory.Cardinal.Cofinality
∀ {f : Ordinal.{u} → Ordinal.{u}}, Ordinal.IsNormal f → ∀ {a o : Ordinal.{u}}, a.IsLimit → ∀ {g : (b : Ordinal.{u}) → b < o → Ordinal.{u}}, a.IsFundamentalSequence o g → (f a).IsFundamentalSequence o fun b hb => f (g b hb) - Ordinal.IsFundamentalSequence.monotone Mathlib.SetTheory.Cardinal.Cofinality
∀ {a o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{u}}, a.IsFundamentalSequence o f → ∀ {i j : Ordinal.{u}} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj - Ordinal.IsFundamentalSequence.strict_mono Mathlib.SetTheory.Cardinal.Cofinality
∀ {a o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{u}}, a.IsFundamentalSequence o f → ∀ {i j : Ordinal.{u}} (hi : i < o) (hj : j < o), i < j → f i hi < f j hj - Ordinal.IsFundamentalSequence.ord_cof Mathlib.SetTheory.Cardinal.Cofinality
∀ {a o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{u}} (hf : a.IsFundamentalSequence o f), a.IsFundamentalSequence a.cof.ord fun i hi => f i ⋯ - Ordinal.IsFundamentalSequence.trans Mathlib.SetTheory.Cardinal.Cofinality
∀ {a o o' : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{u}}, a.IsFundamentalSequence o f → ∀ {g : (b : Ordinal.{u}) → b < o' → Ordinal.{u}} (hg : o.IsFundamentalSequence o' g), a.IsFundamentalSequence o' fun i hi => f (g i hi) ⋯ - MeasureTheory.HasAddFundamentalDomain Mathlib.MeasureTheory.Group.FundamentalDomain
(G : Type u_6) → (α : Type u_7) → [inst : Zero G] → [inst : VAdd G α] → [inst : MeasurableSpace α] → autoParam (MeasureTheory.Measure α) _auto✝ → Prop - MeasureTheory.HasFundamentalDomain Mathlib.MeasureTheory.Group.FundamentalDomain
(G : Type u_6) → (α : Type u_7) → [inst : One G] → [inst : SMul G α] → [inst : MeasurableSpace α] → autoParam (MeasureTheory.Measure α) _auto✝ → Prop - MeasureTheory.addFundamentalFrontier Mathlib.MeasureTheory.Group.FundamentalDomain
(G : Type u_1) → {α : Type u_3} → [inst : AddGroup G] → [inst : AddAction G α] → Set α → Set α - MeasureTheory.addFundamentalInterior Mathlib.MeasureTheory.Group.FundamentalDomain
(G : Type u_1) → {α : Type u_3} → [inst : AddGroup G] → [inst : AddAction G α] → Set α → Set α - MeasureTheory.fundamentalFrontier Mathlib.MeasureTheory.Group.FundamentalDomain
(G : Type u_1) → {α : Type u_3} → [inst : Group G] → [inst : MulAction G α] → Set α → Set α - MeasureTheory.fundamentalInterior Mathlib.MeasureTheory.Group.FundamentalDomain
(G : Type u_1) → {α : Type u_3} → [inst : Group G] → [inst : MulAction G α] → Set α → Set α - MeasureTheory.IsAddFundamentalDomain Mathlib.MeasureTheory.Group.FundamentalDomain
(G : Type u_1) → {α : Type u_2} → [inst : Zero G] → [inst : VAdd G α] → [inst : MeasurableSpace α] → Set α → autoParam (MeasureTheory.Measure α) _auto✝ → Prop - MeasureTheory.IsFundamentalDomain Mathlib.MeasureTheory.Group.FundamentalDomain
(G : Type u_1) → {α : Type u_2} → [inst : One G] → [inst : SMul G α] → [inst : MeasurableSpace α] → Set α → autoParam (MeasureTheory.Measure α) _auto✝ → Prop - MeasureTheory.addFundamentalFrontier_subset Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] {s : Set α}, MeasureTheory.addFundamentalFrontier G s ⊆ s - MeasureTheory.addFundamentalInterior_subset Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] {s : Set α}, MeasureTheory.addFundamentalInterior G s ⊆ s - MeasureTheory.fundamentalFrontier_subset Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] {s : Set α}, MeasureTheory.fundamentalFrontier G s ⊆ s - MeasureTheory.fundamentalInterior_subset Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] {s : Set α}, MeasureTheory.fundamentalInterior G s ⊆ s - MeasureTheory.IsAddFundamentalDomain.nullMeasurableSet Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_2} [inst : Zero G] [inst_1 : VAdd G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : autoParam (MeasureTheory.Measure α) _auto✝}, MeasureTheory.IsAddFundamentalDomain G s μ → MeasureTheory.NullMeasurableSet s μ - MeasureTheory.IsFundamentalDomain.nullMeasurableSet Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_2} [inst : One G] [inst_1 : SMul G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : autoParam (MeasureTheory.Measure α) _auto✝}, MeasureTheory.IsFundamentalDomain G s μ → MeasureTheory.NullMeasurableSet s μ - MeasureTheory.HasAddFundamentalDomain.ExistsIsAddFundamentalDomain Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_6} {α : Type u_7} [inst : Zero G] [inst_1 : VAdd G α] [inst_2 : MeasurableSpace α] {ν : autoParam (MeasureTheory.Measure α) _auto✝} [self : MeasureTheory.HasAddFundamentalDomain G α ν], ∃ s, MeasureTheory.IsAddFundamentalDomain G s ν - MeasureTheory.HasAddFundamentalDomain.mk Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_6} {α : Type u_7} [inst : Zero G] [inst_1 : VAdd G α] [inst_2 : MeasurableSpace α] {ν : autoParam (MeasureTheory.Measure α) _auto✝}, (∃ s, MeasureTheory.IsAddFundamentalDomain G s ν) → MeasureTheory.HasAddFundamentalDomain G α ν - MeasureTheory.HasFundamentalDomain.ExistsIsFundamentalDomain Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_6} {α : Type u_7} [inst : One G] [inst_1 : SMul G α] [inst_2 : MeasurableSpace α] {ν : autoParam (MeasureTheory.Measure α) _auto✝} [self : MeasureTheory.HasFundamentalDomain G α ν], ∃ s, MeasureTheory.IsFundamentalDomain G s ν - MeasureTheory.HasFundamentalDomain.mk Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_6} {α : Type u_7} [inst : One G] [inst_1 : SMul G α] [inst_2 : MeasurableSpace α] {ν : autoParam (MeasureTheory.Measure α) _auto✝}, (∃ s, MeasureTheory.IsFundamentalDomain G s ν) → MeasureTheory.HasFundamentalDomain G α ν - MeasureTheory.addFundamentalFrontier_union_addFundamentalInterior Mathlib.MeasureTheory.Group.FundamentalDomain
∀ (G : Type u_1) {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] (s : Set α), MeasureTheory.addFundamentalFrontier G s ∪ MeasureTheory.addFundamentalInterior G s = s - MeasureTheory.addFundamentalInterior_union_addFundamentalFrontier Mathlib.MeasureTheory.Group.FundamentalDomain
∀ (G : Type u_1) {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] (s : Set α), MeasureTheory.addFundamentalInterior G s ∪ MeasureTheory.addFundamentalFrontier G s = s - MeasureTheory.fundamentalFrontier_union_fundamentalInterior Mathlib.MeasureTheory.Group.FundamentalDomain
∀ (G : Type u_1) {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] (s : Set α), MeasureTheory.fundamentalFrontier G s ∪ MeasureTheory.fundamentalInterior G s = s - MeasureTheory.fundamentalInterior_union_fundamentalFrontier Mathlib.MeasureTheory.Group.FundamentalDomain
∀ (G : Type u_1) {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] (s : Set α), MeasureTheory.fundamentalInterior G s ∪ MeasureTheory.fundamentalFrontier G s = s - MeasureTheory.sdiff_addFundamentalFrontier Mathlib.MeasureTheory.Group.FundamentalDomain
∀ (G : Type u_1) {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] (s : Set α), s \ MeasureTheory.addFundamentalFrontier G s = MeasureTheory.addFundamentalInterior G s - MeasureTheory.sdiff_addFundamentalInterior Mathlib.MeasureTheory.Group.FundamentalDomain
∀ (G : Type u_1) {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] (s : Set α), s \ MeasureTheory.addFundamentalInterior G s = MeasureTheory.addFundamentalFrontier G s - MeasureTheory.sdiff_fundamentalFrontier Mathlib.MeasureTheory.Group.FundamentalDomain
∀ (G : Type u_1) {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] (s : Set α), s \ MeasureTheory.fundamentalFrontier G s = MeasureTheory.fundamentalInterior G s - MeasureTheory.sdiff_fundamentalInterior Mathlib.MeasureTheory.Group.FundamentalDomain
∀ (G : Type u_1) {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] (s : Set α), s \ MeasureTheory.fundamentalInterior G s = MeasureTheory.fundamentalFrontier G s - MeasureTheory.IsAddFundamentalDomain.ae_covers Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_2} [inst : Zero G] [inst_1 : VAdd G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : autoParam (MeasureTheory.Measure α) _auto✝}, MeasureTheory.IsAddFundamentalDomain G s μ → ∀ᵐ (x : α) ∂μ, ∃ g, g +ᵥ x ∈ s - MeasureTheory.IsFundamentalDomain.ae_covers Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_2} [inst : One G] [inst_1 : SMul G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : autoParam (MeasureTheory.Measure α) _auto✝}, MeasureTheory.IsFundamentalDomain G s μ → ∀ᵐ (x : α) ∂μ, ∃ g, g • x ∈ s - MeasureTheory.IsAddFundamentalDomain.aedisjoint Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_2} [inst : Zero G] [inst_1 : VAdd G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : autoParam (MeasureTheory.Measure α) _auto✝}, MeasureTheory.IsAddFundamentalDomain G s μ → Pairwise (MeasureTheory.AEDisjoint μ on fun g => g +ᵥ s) - MeasureTheory.IsFundamentalDomain.aedisjoint Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_2} [inst : One G] [inst_1 : SMul G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : autoParam (MeasureTheory.Measure α) _auto✝}, MeasureTheory.IsFundamentalDomain G s μ → Pairwise (MeasureTheory.AEDisjoint μ on fun g => g • s) - MeasureTheory.disjoint_addFundamentalInterior_addFundamentalFrontier Mathlib.MeasureTheory.Group.FundamentalDomain
∀ (G : Type u_1) {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] (s : Set α), Disjoint (MeasureTheory.addFundamentalInterior G s) (MeasureTheory.addFundamentalFrontier G s) - MeasureTheory.disjoint_fundamentalInterior_fundamentalFrontier Mathlib.MeasureTheory.Group.FundamentalDomain
∀ (G : Type u_1) {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] (s : Set α), Disjoint (MeasureTheory.fundamentalInterior G s) (MeasureTheory.fundamentalFrontier G s) - MeasureTheory.IsAddFundamentalDomain.hasAddFundamentalDomain Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] (ν : MeasureTheory.Measure α) {s : Set α}, MeasureTheory.IsAddFundamentalDomain G s ν → MeasureTheory.HasAddFundamentalDomain G α ν - MeasureTheory.IsFundamentalDomain.hasFundamentalDomain Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] (ν : MeasureTheory.Measure α) {s : Set α}, MeasureTheory.IsFundamentalDomain G s ν → MeasureTheory.HasFundamentalDomain G α ν - MeasureTheory.NullMeasurableSet.addFundamentalFrontier Mathlib.MeasureTheory.Group.FundamentalDomain
∀ (G : Type u_1) {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] (s : Set α) [inst_2 : Countable G] [inst_3 : MeasurableSpace G] [inst_4 : MeasurableSpace α] [inst_5 : MeasurableVAdd G α] {μ : MeasureTheory.Measure α} [inst_6 : MeasureTheory.VAddInvariantMeasure G α μ], MeasureTheory.NullMeasurableSet s μ → MeasureTheory.NullMeasurableSet (MeasureTheory.addFundamentalFrontier G s) μ - MeasureTheory.NullMeasurableSet.addFundamentalInterior Mathlib.MeasureTheory.Group.FundamentalDomain
∀ (G : Type u_1) {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] (s : Set α) [inst_2 : Countable G] [inst_3 : MeasurableSpace G] [inst_4 : MeasurableSpace α] [inst_5 : MeasurableVAdd G α] {μ : MeasureTheory.Measure α} [inst_6 : MeasureTheory.VAddInvariantMeasure G α μ], MeasureTheory.NullMeasurableSet s μ → MeasureTheory.NullMeasurableSet (MeasureTheory.addFundamentalInterior G s) μ - MeasureTheory.NullMeasurableSet.fundamentalFrontier Mathlib.MeasureTheory.Group.FundamentalDomain
∀ (G : Type u_1) {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] (s : Set α) [inst_2 : Countable G] [inst_3 : MeasurableSpace G] [inst_4 : MeasurableSpace α] [inst_5 : MeasurableSMul G α] {μ : MeasureTheory.Measure α} [inst_6 : MeasureTheory.SMulInvariantMeasure G α μ], MeasureTheory.NullMeasurableSet s μ → MeasureTheory.NullMeasurableSet (MeasureTheory.fundamentalFrontier G s) μ - MeasureTheory.NullMeasurableSet.fundamentalInterior Mathlib.MeasureTheory.Group.FundamentalDomain
∀ (G : Type u_1) {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] (s : Set α) [inst_2 : Countable G] [inst_3 : MeasurableSpace G] [inst_4 : MeasurableSpace α] [inst_5 : MeasurableSMul G α] {μ : MeasureTheory.Measure α} [inst_6 : MeasureTheory.SMulInvariantMeasure G α μ], MeasureTheory.NullMeasurableSet s μ → MeasureTheory.NullMeasurableSet (MeasureTheory.fundamentalInterior G s) μ - MeasureTheory.IsAddFundamentalDomain.measure_addFundamentalFrontier Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : Countable G] [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α}, MeasureTheory.IsAddFundamentalDomain G s μ → μ (MeasureTheory.addFundamentalFrontier G s) = 0 - MeasureTheory.IsFundamentalDomain.measure_fundamentalFrontier Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : Countable G] [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α}, MeasureTheory.IsFundamentalDomain G s μ → μ (MeasureTheory.fundamentalFrontier G s) = 0 - MeasureTheory.IsAddFundamentalDomain.mono Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α}, MeasureTheory.IsAddFundamentalDomain G s μ → ∀ {ν : MeasureTheory.Measure α}, ν.AbsolutelyContinuous μ → MeasureTheory.IsAddFundamentalDomain G s ν - MeasureTheory.IsFundamentalDomain.mono Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α}, MeasureTheory.IsFundamentalDomain G s μ → ∀ {ν : MeasureTheory.Measure α}, ν.AbsolutelyContinuous μ → MeasureTheory.IsFundamentalDomain G s ν - MeasureTheory.IsAddFundamentalDomain.mk' Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α}, MeasureTheory.NullMeasurableSet s μ → (∀ (x : α), ∃! g, g +ᵥ x ∈ s) → MeasureTheory.IsAddFundamentalDomain G s μ - MeasureTheory.IsFundamentalDomain.mk' Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α}, MeasureTheory.NullMeasurableSet s μ → (∀ (x : α), ∃! g, g • x ∈ s) → MeasureTheory.IsFundamentalDomain G s μ - MeasureTheory.pairwise_disjoint_addFundamentalInterior Mathlib.MeasureTheory.Group.FundamentalDomain
∀ (G : Type u_1) {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] (s : Set α), Pairwise (Disjoint on fun g => g +ᵥ MeasureTheory.addFundamentalInterior G s) - MeasureTheory.pairwise_disjoint_fundamentalInterior Mathlib.MeasureTheory.Group.FundamentalDomain
∀ (G : Type u_1) {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] (s : Set α), Pairwise (Disjoint on fun g => g • MeasureTheory.fundamentalInterior G s) - MeasureTheory.IsAddFundamentalDomain.iUnion_vadd_ae_eq Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α}, MeasureTheory.IsAddFundamentalDomain G s μ → μ.ae.EventuallyEq (⋃ g, g +ᵥ s) Set.univ - MeasureTheory.IsAddFundamentalDomain.measure_addFundamentalInterior Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : Countable G] [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α}, MeasureTheory.IsAddFundamentalDomain G s μ → μ (MeasureTheory.addFundamentalInterior G s) = μ s - MeasureTheory.IsFundamentalDomain.iUnion_smul_ae_eq Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α}, MeasureTheory.IsFundamentalDomain G s μ → μ.ae.EventuallyEq (⋃ g, g • s) Set.univ - MeasureTheory.IsFundamentalDomain.measure_fundamentalInterior Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : Countable G] [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α}, MeasureTheory.IsFundamentalDomain G s μ → μ (MeasureTheory.fundamentalInterior G s) = μ s - MeasureTheory.IsAddFundamentalDomain.mk Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_2} [inst : Zero G] [inst_1 : VAdd G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : autoParam (MeasureTheory.Measure α) _auto✝}, MeasureTheory.NullMeasurableSet s μ → (∀ᵐ (x : α) ∂μ, ∃ g, g +ᵥ x ∈ s) → Pairwise (MeasureTheory.AEDisjoint μ on fun g => g +ᵥ s) → MeasureTheory.IsAddFundamentalDomain G s μ - MeasureTheory.IsFundamentalDomain.mk Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_2} [inst : One G] [inst_1 : SMul G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : autoParam (MeasureTheory.Measure α) _auto✝}, MeasureTheory.NullMeasurableSet s μ → (∀ᵐ (x : α) ∂μ, ∃ g, g • x ∈ s) → Pairwise (MeasureTheory.AEDisjoint μ on fun g => g • s) → MeasureTheory.IsFundamentalDomain G s μ - MeasureTheory.mem_addFundamentalInterior Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] {s : Set α} {x : α}, x ∈ MeasureTheory.addFundamentalInterior G s ↔ x ∈ s ∧ ∀ (g : G), g ≠ 0 → x ∉ g +ᵥ s - MeasureTheory.mem_fundamentalInterior Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] {s : Set α} {x : α}, x ∈ MeasureTheory.fundamentalInterior G s ↔ x ∈ s ∧ ∀ (g : G), g ≠ 1 → x ∉ g • s - MeasureTheory.mem_addFundamentalFrontier Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] {s : Set α} {x : α}, x ∈ MeasureTheory.addFundamentalFrontier G s ↔ x ∈ s ∧ ∃ g, g ≠ 0 ∧ x ∈ g +ᵥ s - MeasureTheory.mem_fundamentalFrontier Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] {s : Set α} {x : α}, x ∈ MeasureTheory.fundamentalFrontier G s ↔ x ∈ s ∧ ∃ g, g ≠ 1 ∧ x ∈ g • s - MeasureTheory.addFundamentalFrontier.eq_1 Mathlib.MeasureTheory.Group.FundamentalDomain
∀ (G : Type u_1) {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] (s : Set α), MeasureTheory.addFundamentalFrontier G s = s ∩ ⋃ g, ⋃ (_ : g ≠ 0), g +ᵥ s - MeasureTheory.addFundamentalInterior.eq_1 Mathlib.MeasureTheory.Group.FundamentalDomain
∀ (G : Type u_1) {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] (s : Set α), MeasureTheory.addFundamentalInterior G s = s \ ⋃ g, ⋃ (_ : g ≠ 0), g +ᵥ s - MeasureTheory.fundamentalFrontier.eq_1 Mathlib.MeasureTheory.Group.FundamentalDomain
∀ (G : Type u_1) {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] (s : Set α), MeasureTheory.fundamentalFrontier G s = s ∩ ⋃ g, ⋃ (_ : g ≠ 1), g • s - MeasureTheory.fundamentalInterior.eq_1 Mathlib.MeasureTheory.Group.FundamentalDomain
∀ (G : Type u_1) {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] (s : Set α), MeasureTheory.fundamentalInterior G s = s \ ⋃ g, ⋃ (_ : g ≠ 1), g • s - MeasureTheory.IsAddFundamentalDomain.measurePreserving_add_quotient_mk Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {ν : MeasureTheory.Measure α} {𝓕 : Set α}, MeasureTheory.IsAddFundamentalDomain G 𝓕 ν → ∀ (μ : MeasureTheory.Measure (Quotient (AddAction.orbitRel G α))) [inst_3 : MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ], MeasureTheory.MeasurePreserving (Quotient.mk (AddAction.orbitRel G α)) (ν.restrict 𝓕) μ - MeasureTheory.IsFundamentalDomain.measurePreserving_quotient_mk Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {ν : MeasureTheory.Measure α} {𝓕 : Set α}, MeasureTheory.IsFundamentalDomain G 𝓕 ν → ∀ (μ : MeasureTheory.Measure (Quotient (MulAction.orbitRel G α))) [inst_3 : MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ], MeasureTheory.MeasurePreserving (Quotient.mk (MulAction.orbitRel G α)) (ν.restrict 𝓕) μ - MeasureTheory.IsAddFundamentalDomain.nullMeasurableSet_vadd Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableVAdd G α] [inst_5 : MeasureTheory.VAddInvariantMeasure G α μ], MeasureTheory.IsAddFundamentalDomain G s μ → ∀ (g : G), MeasureTheory.NullMeasurableSet (g +ᵥ s) μ - MeasureTheory.IsFundamentalDomain.nullMeasurableSet_smul Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableSMul G α] [inst_5 : MeasureTheory.SMulInvariantMeasure G α μ], MeasureTheory.IsFundamentalDomain G s μ → ∀ (g : G), MeasureTheory.NullMeasurableSet (g • s) μ - MeasureTheory.IsFundamentalDomain.fundamentalInterior Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : Countable G] [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α}, MeasureTheory.IsFundamentalDomain G s μ → ∀ [inst_3 : MeasurableSpace G] [inst_4 : MeasurableSMul G α] [inst_5 : MeasureTheory.SMulInvariantMeasure G α μ], MeasureTheory.IsFundamentalDomain G (MeasureTheory.fundamentalInterior G s) μ - MeasureTheory.IsAddFundamentalDomain.pairwise_aedisjoint_of_ac Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ ν : MeasureTheory.Measure α}, MeasureTheory.IsAddFundamentalDomain G s μ → ν.AbsolutelyContinuous μ → Pairwise fun g₁ g₂ => MeasureTheory.AEDisjoint ν (g₁ +ᵥ s) (g₂ +ᵥ s) - MeasureTheory.IsFundamentalDomain.pairwise_aedisjoint_of_ac Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ ν : MeasureTheory.Measure α}, MeasureTheory.IsFundamentalDomain G s μ → ν.AbsolutelyContinuous μ → Pairwise fun g₁ g₂ => MeasureTheory.AEDisjoint ν (g₁ • s) (g₂ • s) - MeasureTheory.addFundamentalFrontier_vadd Mathlib.MeasureTheory.Group.FundamentalDomain
∀ (G : Type u_1) {H : Type u_2} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] (s : Set α) [inst_2 : AddGroup H] [inst_3 : AddAction H α] [inst_4 : VAddCommClass H G α] (g : H), MeasureTheory.addFundamentalFrontier G (g +ᵥ s) = g +ᵥ MeasureTheory.addFundamentalFrontier G s - MeasureTheory.addFundamentalInterior_vadd Mathlib.MeasureTheory.Group.FundamentalDomain
∀ (G : Type u_1) {H : Type u_2} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] (s : Set α) [inst_2 : AddGroup H] [inst_3 : AddAction H α] [inst_4 : VAddCommClass H G α] (g : H), MeasureTheory.addFundamentalInterior G (g +ᵥ s) = g +ᵥ MeasureTheory.addFundamentalInterior G s - MeasureTheory.fundamentalFrontier_smul Mathlib.MeasureTheory.Group.FundamentalDomain
∀ (G : Type u_1) {H : Type u_2} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] (s : Set α) [inst_2 : Group H] [inst_3 : MulAction H α] [inst_4 : SMulCommClass H G α] (g : H), MeasureTheory.fundamentalFrontier G (g • s) = g • MeasureTheory.fundamentalFrontier G s - MeasureTheory.fundamentalInterior_smul Mathlib.MeasureTheory.Group.FundamentalDomain
∀ (G : Type u_1) {H : Type u_2} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] (s : Set α) [inst_2 : Group H] [inst_3 : MulAction H α] [inst_4 : SMulCommClass H G α] (g : H), MeasureTheory.fundamentalInterior G (g • s) = g • MeasureTheory.fundamentalInterior G s - MeasureTheory.IsAddFundamentalDomain.addQuotientMeasureEqMeasurePreimage_addQuotientMeasure Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {ν : MeasureTheory.Measure α} [inst_3 : Countable G] [inst_4 : MeasurableSpace G] [inst_5 : MeasureTheory.VAddInvariantMeasure G α ν] [inst_6 : MeasurableVAdd G α] {s : Set α}, MeasureTheory.IsAddFundamentalDomain G s ν → MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν (MeasureTheory.Measure.map (Quotient.mk (AddAction.orbitRel G α)) (ν.restrict s)) - MeasureTheory.IsFundamentalDomain.quotientMeasureEqMeasurePreimage_quotientMeasure Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {ν : MeasureTheory.Measure α} [inst_3 : Countable G] [inst_4 : MeasurableSpace G] [inst_5 : MeasureTheory.SMulInvariantMeasure G α ν] [inst_6 : MeasurableSMul G α] {s : Set α}, MeasureTheory.IsFundamentalDomain G s ν → MeasureTheory.QuotientMeasureEqMeasurePreimage ν (MeasureTheory.Measure.map (Quotient.mk (MulAction.orbitRel G α)) (ν.restrict s)) - MeasureTheory.IsAddFundamentalDomain.sum_restrict Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableVAdd G α] [inst_5 : MeasureTheory.VAddInvariantMeasure G α μ] [inst_6 : Countable G], MeasureTheory.IsAddFundamentalDomain G s μ → (MeasureTheory.Measure.sum fun g => μ.restrict (g +ᵥ s)) = μ - MeasureTheory.IsFundamentalDomain.sum_restrict Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableSMul G α] [inst_5 : MeasureTheory.SMulInvariantMeasure G α μ] [inst_6 : Countable G], MeasureTheory.IsFundamentalDomain G s μ → (MeasureTheory.Measure.sum fun g => μ.restrict (g • s)) = μ - MeasureTheory.IsAddFundamentalDomain.covolume_eq_volume Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace G] [inst_3 : MeasurableSpace α] (ν : MeasureTheory.Measure α) [inst_4 : Countable G] [inst_5 : MeasurableVAdd G α] [inst_6 : MeasureTheory.VAddInvariantMeasure G α ν] {s : Set α}, MeasureTheory.IsAddFundamentalDomain G s ν → MeasureTheory.addCovolume G α ν = ν s - MeasureTheory.IsAddFundamentalDomain.measure_ne_zero Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : Countable G] [inst_5 : MeasurableVAdd G α] [inst_6 : MeasureTheory.VAddInvariantMeasure G α μ], μ ≠ 0 → MeasureTheory.IsAddFundamentalDomain G s μ → μ s ≠ 0 - MeasureTheory.IsFundamentalDomain.covolume_eq_volume Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace G] [inst_3 : MeasurableSpace α] (ν : MeasureTheory.Measure α) [inst_4 : Countable G] [inst_5 : MeasurableSMul G α] [inst_6 : MeasureTheory.SMulInvariantMeasure G α ν] {s : Set α}, MeasureTheory.IsFundamentalDomain G s ν → MeasureTheory.covolume G α ν = ν s - MeasureTheory.IsFundamentalDomain.measure_ne_zero Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : Countable G] [inst_5 : MeasurableSMul G α] [inst_6 : MeasureTheory.SMulInvariantMeasure G α μ], μ ≠ 0 → MeasureTheory.IsFundamentalDomain G s μ → μ s ≠ 0 - MeasureTheory.IsAddFundamentalDomain.addProjection_respects_measure Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {ν : MeasureTheory.Measure α} (μ : MeasureTheory.Measure (Quotient (AddAction.orbitRel G α))) [i : MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ] {t : Set α}, MeasureTheory.IsAddFundamentalDomain G t ν → μ = MeasureTheory.Measure.map (Quotient.mk (AddAction.orbitRel G α)) (ν.restrict t) - MeasureTheory.IsFundamentalDomain.projection_respects_measure Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {ν : MeasureTheory.Measure α} (μ : MeasureTheory.Measure (Quotient (MulAction.orbitRel G α))) [i : MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ] {t : Set α}, MeasureTheory.IsFundamentalDomain G t ν → μ = MeasureTheory.Measure.map (Quotient.mk (MulAction.orbitRel G α)) (ν.restrict t) - MeasureTheory.IsAddFundamentalDomain.sum_restrict_of_ac Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableVAdd G α] [inst_5 : MeasureTheory.VAddInvariantMeasure G α μ] [inst_6 : Countable G] {ν : MeasureTheory.Measure α}, MeasureTheory.IsAddFundamentalDomain G s μ → ν.AbsolutelyContinuous μ → (MeasureTheory.Measure.sum fun g => ν.restrict (g +ᵥ s)) = ν - MeasureTheory.IsAddFundamentalDomain.vadd Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableVAdd G α] [inst_5 : MeasureTheory.VAddInvariantMeasure G α μ], MeasureTheory.IsAddFundamentalDomain G s μ → ∀ (g : G), MeasureTheory.IsAddFundamentalDomain G (g +ᵥ s) μ - MeasureTheory.IsFundamentalDomain.smul Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableSMul G α] [inst_5 : MeasureTheory.SMulInvariantMeasure G α μ], MeasureTheory.IsFundamentalDomain G s μ → ∀ (g : G), MeasureTheory.IsFundamentalDomain G (g • s) μ - MeasureTheory.IsFundamentalDomain.sum_restrict_of_ac Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableSMul G α] [inst_5 : MeasureTheory.SMulInvariantMeasure G α μ] [inst_6 : Countable G] {ν : MeasureTheory.Measure α}, MeasureTheory.IsFundamentalDomain G s μ → ν.AbsolutelyContinuous μ → (MeasureTheory.Measure.sum fun g => ν.restrict (g • s)) = ν - MeasureTheory.IsAddFundamentalDomain.lintegral_eq_tsum'' Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableVAdd G α] [inst_5 : MeasureTheory.VAddInvariantMeasure G α μ] [inst_6 : Countable G], MeasureTheory.IsAddFundamentalDomain G s μ → ∀ (f : α → ENNReal), ∫⁻ (x : α), f x ∂μ = ∑' (g : G), ∫⁻ (x : α) in s, f (g +ᵥ x) ∂μ - MeasureTheory.IsFundamentalDomain.lintegral_eq_tsum'' Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableSMul G α] [inst_5 : MeasureTheory.SMulInvariantMeasure G α μ] [inst_6 : Countable G], MeasureTheory.IsFundamentalDomain G s μ → ∀ (f : α → ENNReal), ∫⁻ (x : α), f x ∂μ = ∑' (g : G), ∫⁻ (x : α) in s, f (g • x) ∂μ - MeasureTheory.IsAddFundamentalDomain.measure_eq Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s t : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableVAdd G α] [inst_5 : MeasureTheory.VAddInvariantMeasure G α μ] [inst_6 : Countable G], MeasureTheory.IsAddFundamentalDomain G s μ → MeasureTheory.IsAddFundamentalDomain G t μ → μ s = μ t - MeasureTheory.IsFundamentalDomain.measure_eq Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s t : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableSMul G α] [inst_5 : MeasureTheory.SMulInvariantMeasure G α μ] [inst_6 : Countable G], MeasureTheory.IsFundamentalDomain G s μ → MeasureTheory.IsFundamentalDomain G t μ → μ s = μ t - MeasureTheory.IsAddFundamentalDomain.essSup_measure_restrict Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableVAdd G α] [inst_5 : MeasureTheory.VAddInvariantMeasure G α μ] [inst_6 : Countable G], MeasureTheory.IsAddFundamentalDomain G s μ → ∀ {f : α → ENNReal}, (∀ (γ : G) (x : α), f (γ +ᵥ x) = f x) → essSup f (μ.restrict s) = essSup f μ - MeasureTheory.IsAddFundamentalDomain.lintegral_eq_tsum Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableVAdd G α] [inst_5 : MeasureTheory.VAddInvariantMeasure G α μ] [inst_6 : Countable G], MeasureTheory.IsAddFundamentalDomain G s μ → ∀ (f : α → ENNReal), ∫⁻ (x : α), f x ∂μ = ∑' (g : G), ∫⁻ (x : α) in g +ᵥ s, f x ∂μ - MeasureTheory.IsFundamentalDomain.essSup_measure_restrict Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableSMul G α] [inst_5 : MeasureTheory.SMulInvariantMeasure G α μ] [inst_6 : Countable G], MeasureTheory.IsFundamentalDomain G s μ → ∀ {f : α → ENNReal}, (∀ (γ : G) (x : α), f (γ • x) = f x) → essSup f (μ.restrict s) = essSup f μ - MeasureTheory.IsFundamentalDomain.lintegral_eq_tsum Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableSMul G α] [inst_5 : MeasureTheory.SMulInvariantMeasure G α μ] [inst_6 : Countable G], MeasureTheory.IsFundamentalDomain G s μ → ∀ (f : α → ENNReal), ∫⁻ (x : α), f x ∂μ = ∑' (g : G), ∫⁻ (x : α) in g • s, f x ∂μ - MeasureTheory.instSigmaFiniteQuotientOrbitRelOfHasFundamentalDomainOfQuotientMeasureEqMeasurePreimageVolume Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasureTheory.MeasureSpace α] [inst_3 : Countable G] [inst_4 : MeasurableSpace G] [inst_5 : MeasureTheory.SMulInvariantMeasure G α MeasureTheory.volume] [inst_6 : MeasurableSMul G α] [inst_7 : MeasureTheory.SigmaFinite MeasureTheory.volume] [inst_8 : MeasureTheory.HasFundamentalDomain G α MeasureTheory.volume] (μ : MeasureTheory.Measure (Quotient (MulAction.orbitRel G α))) [inst_9 : MeasureTheory.QuotientMeasureEqMeasurePreimage MeasureTheory.volume μ], MeasureTheory.SigmaFinite μ - MeasureTheory.IsAddFundamentalDomain.lintegral_eq_tsum' Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableVAdd G α] [inst_5 : MeasureTheory.VAddInvariantMeasure G α μ] [inst_6 : Countable G], MeasureTheory.IsAddFundamentalDomain G s μ → ∀ (f : α → ENNReal), ∫⁻ (x : α), f x ∂μ = ∑' (g : G), ∫⁻ (x : α) in s, f (-g +ᵥ x) ∂μ - MeasureTheory.IsFundamentalDomain.lintegral_eq_tsum' Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableSMul G α] [inst_5 : MeasureTheory.SMulInvariantMeasure G α μ] [inst_6 : Countable G], MeasureTheory.IsFundamentalDomain G s μ → ∀ (f : α → ENNReal), ∫⁻ (x : α), f x ∂μ = ∑' (g : G), ∫⁻ (x : α) in s, f (g⁻¹ • x) ∂μ - MeasureTheory.IsAddFundamentalDomain.lintegral_eq_tsum_of_ac Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableVAdd G α] [inst_5 : MeasureTheory.VAddInvariantMeasure G α μ] [inst_6 : Countable G] {ν : MeasureTheory.Measure α}, MeasureTheory.IsAddFundamentalDomain G s μ → ν.AbsolutelyContinuous μ → ∀ (f : α → ENNReal), ∫⁻ (x : α), f x ∂ν = ∑' (g : G), ∫⁻ (x : α) in g +ᵥ s, f x ∂ν - MeasureTheory.IsFundamentalDomain.lintegral_eq_tsum_of_ac Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableSMul G α] [inst_5 : MeasureTheory.SMulInvariantMeasure G α μ] [inst_6 : Countable G] {ν : MeasureTheory.Measure α}, MeasureTheory.IsFundamentalDomain G s μ → ν.AbsolutelyContinuous μ → ∀ (f : α → ENNReal), ∫⁻ (x : α), f x ∂ν = ∑' (g : G), ∫⁻ (x : α) in g • s, f x ∂ν - MeasureTheory.IsAddFundamentalDomain.restrict_restrict Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableVAdd G α] [inst_5 : MeasureTheory.VAddInvariantMeasure G α μ], MeasureTheory.IsAddFundamentalDomain G s μ → ∀ (g : G) (t : Set α), (μ.restrict t).restrict (g +ᵥ s) = μ.restrict ((g +ᵥ s) ∩ t) - MeasureTheory.IsAddFundamentalDomain.set_lintegral_eq_tsum Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableVAdd G α] [inst_5 : MeasureTheory.VAddInvariantMeasure G α μ] [inst_6 : Countable G], MeasureTheory.IsAddFundamentalDomain G s μ → ∀ (f : α → ENNReal) (t : Set α), ∫⁻ (x : α) in t, f x ∂μ = ∑' (g : G), ∫⁻ (x : α) in t ∩ (g +ᵥ s), f x ∂μ - MeasureTheory.IsFundamentalDomain.restrict_restrict Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableSMul G α] [inst_5 : MeasureTheory.SMulInvariantMeasure G α μ], MeasureTheory.IsFundamentalDomain G s μ → ∀ (g : G) (t : Set α), (μ.restrict t).restrict (g • s) = μ.restrict (g • s ∩ t) - MeasureTheory.IsFundamentalDomain.set_lintegral_eq_tsum Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableSMul G α] [inst_5 : MeasureTheory.SMulInvariantMeasure G α μ] [inst_6 : Countable G], MeasureTheory.IsFundamentalDomain G s μ → ∀ (f : α → ENNReal) (t : Set α), ∫⁻ (x : α) in t, f x ∂μ = ∑' (g : G), ∫⁻ (x : α) in t ∩ g • s, f x ∂μ - MeasureTheory.IsAddFundamentalDomain.addQuotientMeasureEqMeasurePreimage Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {ν : MeasureTheory.Measure α} [inst_3 : Countable G] [inst_4 : MeasurableSpace G] [inst_5 : MeasureTheory.VAddInvariantMeasure G α ν] [inst_6 : MeasurableVAdd G α] {μ : MeasureTheory.Measure (Quotient (AddAction.orbitRel G α))} {s : Set α}, MeasureTheory.IsAddFundamentalDomain G s ν → μ = MeasureTheory.Measure.map (Quotient.mk (AddAction.orbitRel G α)) (ν.restrict s) → MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ - MeasureTheory.IsFundamentalDomain.quotientMeasureEqMeasurePreimage Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {ν : MeasureTheory.Measure α} [inst_3 : Countable G] [inst_4 : MeasurableSpace G] [inst_5 : MeasureTheory.SMulInvariantMeasure G α ν] [inst_6 : MeasurableSMul G α] {μ : MeasureTheory.Measure (Quotient (MulAction.orbitRel G α))} {s : Set α}, MeasureTheory.IsFundamentalDomain G s ν → μ = MeasureTheory.Measure.map (Quotient.mk (MulAction.orbitRel G α)) (ν.restrict s) → MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ - MeasureTheory.IsAddFundamentalDomain.integrableOn_iff Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} {E : Type u_5} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] [inst_3 : NormedAddCommGroup E] {s t : Set α} {μ : MeasureTheory.Measure α} [inst_4 : MeasurableSpace G] [inst_5 : MeasurableVAdd G α] [inst_6 : MeasureTheory.VAddInvariantMeasure G α μ] [inst_7 : Countable G], MeasureTheory.IsAddFundamentalDomain G s μ → MeasureTheory.IsAddFundamentalDomain G t μ → ∀ {f : α → E}, (∀ (g : G) (x : α), f (g +ᵥ x) = f x) → (MeasureTheory.IntegrableOn f s μ ↔ MeasureTheory.IntegrableOn f t μ) - MeasureTheory.IsAddFundamentalDomain.preimage_of_equiv Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {H : Type u_2} {α : Type u_3} {β : Type u_4} [inst : AddGroup G] [inst_1 : AddGroup H] [inst_2 : AddAction G α] [inst_3 : MeasurableSpace α] [inst_4 : AddAction H β] [inst_5 : MeasurableSpace β] {s : Set α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β}, MeasureTheory.IsAddFundamentalDomain G s μ → ∀ {f : β → α}, MeasureTheory.Measure.QuasiMeasurePreserving f ν μ → ∀ {e : G → H}, Function.Bijective e → (∀ (g : G), Function.Semiconj f (fun x => e g +ᵥ x) fun x => g +ᵥ x) → MeasureTheory.IsAddFundamentalDomain H (f ⁻¹' s) ν - MeasureTheory.IsFundamentalDomain.integrableOn_iff Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} {E : Type u_5} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] [inst_3 : NormedAddCommGroup E] {s t : Set α} {μ : MeasureTheory.Measure α} [inst_4 : MeasurableSpace G] [inst_5 : MeasurableSMul G α] [inst_6 : MeasureTheory.SMulInvariantMeasure G α μ] [inst_7 : Countable G], MeasureTheory.IsFundamentalDomain G s μ → MeasureTheory.IsFundamentalDomain G t μ → ∀ {f : α → E}, (∀ (g : G) (x : α), f (g • x) = f x) → (MeasureTheory.IntegrableOn f s μ ↔ MeasureTheory.IntegrableOn f t μ) - MeasureTheory.IsFundamentalDomain.preimage_of_equiv Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {H : Type u_2} {α : Type u_3} {β : Type u_4} [inst : Group G] [inst_1 : Group H] [inst_2 : MulAction G α] [inst_3 : MeasurableSpace α] [inst_4 : MulAction H β] [inst_5 : MeasurableSpace β] {s : Set α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β}, MeasureTheory.IsFundamentalDomain G s μ → ∀ {f : β → α}, MeasureTheory.Measure.QuasiMeasurePreserving f ν μ → ∀ {e : G → H}, Function.Bijective e → (∀ (g : G), Function.Semiconj f (fun x => e g • x) fun x => g • x) → MeasureTheory.IsFundamentalDomain H (f ⁻¹' s) ν - MeasureTheory.IsAddFundamentalDomain.measure_eq_tsum Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableVAdd G α] [inst_5 : MeasureTheory.VAddInvariantMeasure G α μ] [inst_6 : Countable G], MeasureTheory.IsAddFundamentalDomain G s μ → ∀ (t : Set α), μ t = ∑' (g : G), μ ((g +ᵥ t) ∩ s) - MeasureTheory.IsAddFundamentalDomain.measure_eq_tsum' Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableVAdd G α] [inst_5 : MeasureTheory.VAddInvariantMeasure G α μ] [inst_6 : Countable G], MeasureTheory.IsAddFundamentalDomain G s μ → ∀ (t : Set α), μ t = ∑' (g : G), μ (t ∩ (g +ᵥ s)) - MeasureTheory.IsFundamentalDomain.measure_eq_tsum Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableSMul G α] [inst_5 : MeasureTheory.SMulInvariantMeasure G α μ] [inst_6 : Countable G], MeasureTheory.IsFundamentalDomain G s μ → ∀ (t : Set α), μ t = ∑' (g : G), μ (g • t ∩ s) - MeasureTheory.IsFundamentalDomain.measure_eq_tsum' Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableSMul G α] [inst_5 : MeasureTheory.SMulInvariantMeasure G α μ] [inst_6 : Countable G], MeasureTheory.IsFundamentalDomain G s μ → ∀ (t : Set α), μ t = ∑' (g : G), μ (t ∩ g • s) - MeasureTheory.IsAddFundamentalDomain.set_lintegral_eq Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s t : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableVAdd G α] [inst_5 : MeasureTheory.VAddInvariantMeasure G α μ] [inst_6 : Countable G], MeasureTheory.IsAddFundamentalDomain G s μ → MeasureTheory.IsAddFundamentalDomain G t μ → ∀ (f : α → ENNReal), (∀ (g : G) (x : α), f (g +ᵥ x) = f x) → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in t, f x ∂μ - MeasureTheory.IsFundamentalDomain.set_lintegral_eq Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s t : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableSMul G α] [inst_5 : MeasureTheory.SMulInvariantMeasure G α μ] [inst_6 : Countable G], MeasureTheory.IsFundamentalDomain G s μ → MeasureTheory.IsFundamentalDomain G t μ → ∀ (f : α → ENNReal), (∀ (g : G) (x : α), f (g • x) = f x) → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in t, f x ∂μ - MeasureTheory.IsAddFundamentalDomain.hasFiniteIntegral_on_iff Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} {E : Type u_5} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] [inst_3 : NormedAddCommGroup E] {s t : Set α} {μ : MeasureTheory.Measure α} [inst_4 : MeasurableSpace G] [inst_5 : MeasurableVAdd G α] [inst_6 : MeasureTheory.VAddInvariantMeasure G α μ] [inst_7 : Countable G], MeasureTheory.IsAddFundamentalDomain G s μ → MeasureTheory.IsAddFundamentalDomain G t μ → ∀ {f : α → E}, (∀ (g : G) (x : α), f (g +ᵥ x) = f x) → (MeasureTheory.HasFiniteIntegral f (μ.restrict s) ↔ MeasureTheory.HasFiniteIntegral f (μ.restrict t)) - MeasureTheory.IsAddFundamentalDomain.vadd_of_comm Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} {G' : Type u_6} [inst_3 : AddGroup G'] [inst_4 : AddAction G' α] [inst_5 : MeasurableSpace G'] [inst_6 : MeasurableVAdd G' α] [inst_7 : MeasureTheory.VAddInvariantMeasure G' α μ] [inst_8 : VAddCommClass G' G α], MeasureTheory.IsAddFundamentalDomain G s μ → ∀ (g : G'), MeasureTheory.IsAddFundamentalDomain G (g +ᵥ s) μ - MeasureTheory.IsFundamentalDomain.hasFiniteIntegral_on_iff Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} {E : Type u_5} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] [inst_3 : NormedAddCommGroup E] {s t : Set α} {μ : MeasureTheory.Measure α} [inst_4 : MeasurableSpace G] [inst_5 : MeasurableSMul G α] [inst_6 : MeasureTheory.SMulInvariantMeasure G α μ] [inst_7 : Countable G], MeasureTheory.IsFundamentalDomain G s μ → MeasureTheory.IsFundamentalDomain G t μ → ∀ {f : α → E}, (∀ (g : G) (x : α), f (g • x) = f x) → (MeasureTheory.HasFiniteIntegral f (μ.restrict s) ↔ MeasureTheory.HasFiniteIntegral f (μ.restrict t)) - MeasureTheory.IsFundamentalDomain.smul_of_comm Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} {G' : Type u_6} [inst_3 : Group G'] [inst_4 : MulAction G' α] [inst_5 : MeasurableSpace G'] [inst_6 : MeasurableSMul G' α] [inst_7 : MeasureTheory.SMulInvariantMeasure G' α μ] [inst_8 : SMulCommClass G' G α], MeasureTheory.IsFundamentalDomain G s μ → ∀ (g : G'), MeasureTheory.IsFundamentalDomain G (g • s) μ - MeasureTheory.IsAddFundamentalDomain.addQuotientMeasureEqMeasurePreimage_of_zero Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {ν : MeasureTheory.Measure α} [inst_3 : Countable G] [inst_4 : MeasurableSpace G] [inst_5 : MeasureTheory.VAddInvariantMeasure G α ν] [inst_6 : MeasurableVAdd G α] {s : Set α}, MeasureTheory.IsAddFundamentalDomain G s ν → ν s = 0 → MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν 0 - MeasureTheory.IsAddFundamentalDomain.integral_eq_tsum'' Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} {E : Type u_5} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] [inst_3 : NormedAddCommGroup E] {s : Set α} {μ : MeasureTheory.Measure α} [inst_4 : MeasurableSpace G] [inst_5 : MeasurableVAdd G α] [inst_6 : MeasureTheory.VAddInvariantMeasure G α μ] [inst_7 : Countable G] [inst_8 : NormedSpace ℝ E], MeasureTheory.IsAddFundamentalDomain G s μ → ∀ (f : α → E), MeasureTheory.Integrable f μ → ∫ (x : α), f x ∂μ = ∑' (g : G), ∫ (x : α) in s, f (g +ᵥ x) ∂μ - MeasureTheory.IsFundamentalDomain.integral_eq_tsum'' Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} {E : Type u_5} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] [inst_3 : NormedAddCommGroup E] {s : Set α} {μ : MeasureTheory.Measure α} [inst_4 : MeasurableSpace G] [inst_5 : MeasurableSMul G α] [inst_6 : MeasureTheory.SMulInvariantMeasure G α μ] [inst_7 : Countable G] [inst_8 : NormedSpace ℝ E], MeasureTheory.IsFundamentalDomain G s μ → ∀ (f : α → E), MeasureTheory.Integrable f μ → ∫ (x : α), f x ∂μ = ∑' (g : G), ∫ (x : α) in s, f (g • x) ∂μ - MeasureTheory.IsFundamentalDomain.quotientMeasureEqMeasurePreimage_of_zero Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {ν : MeasureTheory.Measure α} [inst_3 : Countable G] [inst_4 : MeasurableSpace G] [inst_5 : MeasureTheory.SMulInvariantMeasure G α ν] [inst_6 : MeasurableSMul G α] {s : Set α}, MeasureTheory.IsFundamentalDomain G s ν → ν s = 0 → MeasureTheory.QuotientMeasureEqMeasurePreimage ν 0 - MeasureTheory.IsAddFundamentalDomain.measure_zero_of_invariant Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableVAdd G α] [inst_5 : MeasureTheory.VAddInvariantMeasure G α μ] [inst_6 : Countable G], MeasureTheory.IsAddFundamentalDomain G s μ → ∀ (t : Set α), (∀ (g : G), g +ᵥ t = t) → μ (t ∩ s) = 0 → μ t = 0 - MeasureTheory.IsFundamentalDomain.measure_zero_of_invariant Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableSMul G α] [inst_5 : MeasureTheory.SMulInvariantMeasure G α μ] [inst_6 : Countable G], MeasureTheory.IsFundamentalDomain G s μ → ∀ (t : Set α), (∀ (g : G), g • t = t) → μ (t ∩ s) = 0 → μ t = 0 - MeasureTheory.IsAddFundamentalDomain.aEStronglyMeasurable_on_iff Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s t : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableVAdd G α] [inst_5 : MeasureTheory.VAddInvariantMeasure G α μ] [inst_6 : Countable G] {β : Type u_6} [inst_7 : TopologicalSpace β] [inst_8 : TopologicalSpace.PseudoMetrizableSpace β], MeasureTheory.IsAddFundamentalDomain G s μ → MeasureTheory.IsAddFundamentalDomain G t μ → ∀ {f : α → β}, (∀ (g : G) (x : α), f (g +ᵥ x) = f x) → (MeasureTheory.AEStronglyMeasurable f (μ.restrict s) ↔ MeasureTheory.AEStronglyMeasurable f (μ.restrict t)) - MeasureTheory.IsAddFundamentalDomain.mk'' Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α}, MeasureTheory.NullMeasurableSet s μ → (∀ᵐ (x : α) ∂μ, ∃ g, g +ᵥ x ∈ s) → (∀ (g : G), g ≠ 0 → MeasureTheory.AEDisjoint μ (g +ᵥ s) s) → (∀ (g : G), MeasureTheory.Measure.QuasiMeasurePreserving (fun x => g +ᵥ x) μ μ) → MeasureTheory.IsAddFundamentalDomain G s μ - MeasureTheory.IsFundamentalDomain.aEStronglyMeasurable_on_iff Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s t : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableSMul G α] [inst_5 : MeasureTheory.SMulInvariantMeasure G α μ] [inst_6 : Countable G] {β : Type u_6} [inst_7 : TopologicalSpace β] [inst_8 : TopologicalSpace.PseudoMetrizableSpace β], MeasureTheory.IsFundamentalDomain G s μ → MeasureTheory.IsFundamentalDomain G t μ → ∀ {f : α → β}, (∀ (g : G) (x : α), f (g • x) = f x) → (MeasureTheory.AEStronglyMeasurable f (μ.restrict s) ↔ MeasureTheory.AEStronglyMeasurable f (μ.restrict t)) - MeasureTheory.IsFundamentalDomain.mk'' Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α}, MeasureTheory.NullMeasurableSet s μ → (∀ᵐ (x : α) ∂μ, ∃ g, g • x ∈ s) → (∀ (g : G), g ≠ 1 → MeasureTheory.AEDisjoint μ (g • s) s) → (∀ (g : G), MeasureTheory.Measure.QuasiMeasurePreserving (fun x => g • x) μ μ) → MeasureTheory.IsFundamentalDomain G s μ - MeasureTheory.IsAddFundamentalDomain.measure_eq_tsum_of_ac Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableVAdd G α] [inst_5 : MeasureTheory.VAddInvariantMeasure G α μ] [inst_6 : Countable G] {ν : MeasureTheory.Measure α}, MeasureTheory.IsAddFundamentalDomain G s μ → ν.AbsolutelyContinuous μ → ∀ (t : Set α), ν t = ∑' (g : G), ν (t ∩ (g +ᵥ s)) - MeasureTheory.IsFundamentalDomain.measure_eq_tsum_of_ac Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableSMul G α] [inst_5 : MeasureTheory.SMulInvariantMeasure G α μ] [inst_6 : Countable G] {ν : MeasureTheory.Measure α}, MeasureTheory.IsFundamentalDomain G s μ → ν.AbsolutelyContinuous μ → ∀ (t : Set α), ν t = ∑' (g : G), ν (t ∩ g • s) - MeasureTheory.IsAddFundamentalDomain.integral_eq_tsum Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} {E : Type u_5} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] [inst_3 : NormedAddCommGroup E] {s : Set α} {μ : MeasureTheory.Measure α} [inst_4 : MeasurableSpace G] [inst_5 : MeasurableVAdd G α] [inst_6 : MeasureTheory.VAddInvariantMeasure G α μ] [inst_7 : Countable G] [inst_8 : NormedSpace ℝ E], MeasureTheory.IsAddFundamentalDomain G s μ → ∀ (f : α → E), MeasureTheory.Integrable f μ → ∫ (x : α), f x ∂μ = ∑' (g : G), ∫ (x : α) in g +ᵥ s, f x ∂μ - MeasureTheory.IsFundamentalDomain.integral_eq_tsum Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} {E : Type u_5} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] [inst_3 : NormedAddCommGroup E] {s : Set α} {μ : MeasureTheory.Measure α} [inst_4 : MeasurableSpace G] [inst_5 : MeasurableSMul G α] [inst_6 : MeasureTheory.SMulInvariantMeasure G α μ] [inst_7 : Countable G] [inst_8 : NormedSpace ℝ E], MeasureTheory.IsFundamentalDomain G s μ → ∀ (f : α → E), MeasureTheory.Integrable f μ → ∫ (x : α), f x ∂μ = ∑' (g : G), ∫ (x : α) in g • s, f x ∂μ - MeasureTheory.IsAddFundamentalDomain.measure_eq_card_smul_of_vadd_ae_eq_self Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableVAdd G α] [inst_5 : MeasureTheory.VAddInvariantMeasure G α μ] [inst_6 : Countable G] [inst_7 : Finite G], MeasureTheory.IsAddFundamentalDomain G s μ → ∀ (t : Set α), (∀ (g : G), μ.ae.EventuallyEq (g +ᵥ t) t) → μ t = Nat.card G • μ (t ∩ s) - MeasureTheory.IsFundamentalDomain.measure_eq_card_smul_of_smul_ae_eq_self Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableSMul G α] [inst_5 : MeasureTheory.SMulInvariantMeasure G α μ] [inst_6 : Countable G] [inst_7 : Finite G], MeasureTheory.IsFundamentalDomain G s μ → ∀ (t : Set α), (∀ (g : G), μ.ae.EventuallyEq (g • t) t) → μ t = Nat.card G • μ (t ∩ s) - MeasureTheory.IsAddFundamentalDomain.integral_eq_tsum' Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} {E : Type u_5} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] [inst_3 : NormedAddCommGroup E] {s : Set α} {μ : MeasureTheory.Measure α} [inst_4 : MeasurableSpace G] [inst_5 : MeasurableVAdd G α] [inst_6 : MeasureTheory.VAddInvariantMeasure G α μ] [inst_7 : Countable G] [inst_8 : NormedSpace ℝ E], MeasureTheory.IsAddFundamentalDomain G s μ → ∀ (f : α → E), MeasureTheory.Integrable f μ → ∫ (x : α), f x ∂μ = ∑' (g : G), ∫ (x : α) in s, f (-g +ᵥ x) ∂μ - MeasureTheory.IsFundamentalDomain.integral_eq_tsum' Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} {E : Type u_5} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] [inst_3 : NormedAddCommGroup E] {s : Set α} {μ : MeasureTheory.Measure α} [inst_4 : MeasurableSpace G] [inst_5 : MeasurableSMul G α] [inst_6 : MeasureTheory.SMulInvariantMeasure G α μ] [inst_7 : Countable G] [inst_8 : NormedSpace ℝ E], MeasureTheory.IsFundamentalDomain G s μ → ∀ (f : α → E), MeasureTheory.Integrable f μ → ∫ (x : α), f x ∂μ = ∑' (g : G), ∫ (x : α) in s, f (g⁻¹ • x) ∂μ - MeasureTheory.IsAddFundamentalDomain.measure_le_of_pairwise_disjoint Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s t : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableVAdd G α] [inst_5 : MeasureTheory.VAddInvariantMeasure G α μ] [inst_6 : Countable G], MeasureTheory.IsAddFundamentalDomain G s μ → MeasureTheory.NullMeasurableSet t μ → Pairwise (MeasureTheory.AEDisjoint μ on fun g => (g +ᵥ t) ∩ s) → μ t ≤ μ s - MeasureTheory.IsFundamentalDomain.measure_le_of_pairwise_disjoint Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s t : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableSMul G α] [inst_5 : MeasureTheory.SMulInvariantMeasure G α μ] [inst_6 : Countable G], MeasureTheory.IsFundamentalDomain G s μ → MeasureTheory.NullMeasurableSet t μ → Pairwise (MeasureTheory.AEDisjoint μ on fun g => g • t ∩ s) → μ t ≤ μ s - MeasureTheory.IsAddFundamentalDomain.setIntegral_eq Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} {E : Type u_5} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] [inst_3 : NormedAddCommGroup E] {s t : Set α} {μ : MeasureTheory.Measure α} [inst_4 : MeasurableSpace G] [inst_5 : MeasurableVAdd G α] [inst_6 : MeasureTheory.VAddInvariantMeasure G α μ] [inst_7 : Countable G] [inst_8 : NormedSpace ℝ E], MeasureTheory.IsAddFundamentalDomain G s μ → MeasureTheory.IsAddFundamentalDomain G t μ → ∀ {f : α → E}, (∀ (g : G) (x : α), f (g +ᵥ x) = f x) → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in t, f x ∂μ - MeasureTheory.IsFundamentalDomain.setIntegral_eq Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} {E : Type u_5} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] [inst_3 : NormedAddCommGroup E] {s t : Set α} {μ : MeasureTheory.Measure α} [inst_4 : MeasurableSpace G] [inst_5 : MeasurableSMul G α] [inst_6 : MeasureTheory.SMulInvariantMeasure G α μ] [inst_7 : Countable G] [inst_8 : NormedSpace ℝ E], MeasureTheory.IsFundamentalDomain G s μ → MeasureTheory.IsFundamentalDomain G t μ → ∀ {f : α → E}, (∀ (g : G) (x : α), f (g • x) = f x) → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in t, f x ∂μ - MeasureTheory.IsFundamentalDomain.set_integral_eq Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} {E : Type u_5} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] [inst_3 : NormedAddCommGroup E] {s t : Set α} {μ : MeasureTheory.Measure α} [inst_4 : MeasurableSpace G] [inst_5 : MeasurableSMul G α] [inst_6 : MeasureTheory.SMulInvariantMeasure G α μ] [inst_7 : Countable G] [inst_8 : NormedSpace ℝ E], MeasureTheory.IsFundamentalDomain G s μ → MeasureTheory.IsFundamentalDomain G t μ → ∀ {f : α → E}, (∀ (g : G) (x : α), f (g • x) = f x) → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in t, f x ∂μ - MeasureTheory.IsAddFundamentalDomain.integral_eq_tsum_of_ac Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} {E : Type u_5} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] [inst_3 : NormedAddCommGroup E] {s : Set α} {μ : MeasureTheory.Measure α} [inst_4 : MeasurableSpace G] [inst_5 : MeasurableVAdd G α] [inst_6 : MeasureTheory.VAddInvariantMeasure G α μ] [inst_7 : Countable G] {ν : MeasureTheory.Measure α} [inst_8 : NormedSpace ℝ E], MeasureTheory.IsAddFundamentalDomain G s μ → ν.AbsolutelyContinuous μ → ∀ (f : α → E), MeasureTheory.Integrable f ν → ∫ (x : α), f x ∂ν = ∑' (g : G), ∫ (x : α) in g +ᵥ s, f x ∂ν - MeasureTheory.IsFundamentalDomain.integral_eq_tsum_of_ac Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} {E : Type u_5} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] [inst_3 : NormedAddCommGroup E] {s : Set α} {μ : MeasureTheory.Measure α} [inst_4 : MeasurableSpace G] [inst_5 : MeasurableSMul G α] [inst_6 : MeasureTheory.SMulInvariantMeasure G α μ] [inst_7 : Countable G] {ν : MeasureTheory.Measure α} [inst_8 : NormedSpace ℝ E], MeasureTheory.IsFundamentalDomain G s μ → ν.AbsolutelyContinuous μ → ∀ (f : α → E), MeasureTheory.Integrable f ν → ∫ (x : α), f x ∂ν = ∑' (g : G), ∫ (x : α) in g • s, f x ∂ν - MeasureTheory.IsAddFundamentalDomain.setIntegral_eq_tsum Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} {E : Type u_5} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] [inst_3 : NormedAddCommGroup E] {s : Set α} {μ : MeasureTheory.Measure α} [inst_4 : MeasurableSpace G] [inst_5 : MeasurableVAdd G α] [inst_6 : MeasureTheory.VAddInvariantMeasure G α μ] [inst_7 : Countable G] [inst_8 : NormedSpace ℝ E], MeasureTheory.IsAddFundamentalDomain G s μ → ∀ {f : α → E} {t : Set α}, MeasureTheory.IntegrableOn f t μ → ∫ (x : α) in t, f x ∂μ = ∑' (g : G), ∫ (x : α) in t ∩ (g +ᵥ s), f x ∂μ - MeasureTheory.IsAddFundamentalDomain.set_lintegral_eq_tsum' Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableVAdd G α] [inst_5 : MeasureTheory.VAddInvariantMeasure G α μ] [inst_6 : Countable G], MeasureTheory.IsAddFundamentalDomain G s μ → ∀ (f : α → ENNReal) (t : Set α), ∫⁻ (x : α) in t, f x ∂μ = ∑' (g : G), ∫⁻ (x : α) in (g +ᵥ t) ∩ s, f (-g +ᵥ x) ∂μ - MeasureTheory.IsFundamentalDomain.setIntegral_eq_tsum Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} {E : Type u_5} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] [inst_3 : NormedAddCommGroup E] {s : Set α} {μ : MeasureTheory.Measure α} [inst_4 : MeasurableSpace G] [inst_5 : MeasurableSMul G α] [inst_6 : MeasureTheory.SMulInvariantMeasure G α μ] [inst_7 : Countable G] [inst_8 : NormedSpace ℝ E], MeasureTheory.IsFundamentalDomain G s μ → ∀ {f : α → E} {t : Set α}, MeasureTheory.IntegrableOn f t μ → ∫ (x : α) in t, f x ∂μ = ∑' (g : G), ∫ (x : α) in t ∩ g • s, f x ∂μ - MeasureTheory.IsFundamentalDomain.set_integral_eq_tsum Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} {E : Type u_5} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] [inst_3 : NormedAddCommGroup E] {s : Set α} {μ : MeasureTheory.Measure α} [inst_4 : MeasurableSpace G] [inst_5 : MeasurableSMul G α] [inst_6 : MeasureTheory.SMulInvariantMeasure G α μ] [inst_7 : Countable G] [inst_8 : NormedSpace ℝ E], MeasureTheory.IsFundamentalDomain G s μ → ∀ {f : α → E} {t : Set α}, MeasureTheory.IntegrableOn f t μ → ∫ (x : α) in t, f x ∂μ = ∑' (g : G), ∫ (x : α) in t ∩ g • s, f x ∂μ - MeasureTheory.IsFundamentalDomain.set_lintegral_eq_tsum' Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableSMul G α] [inst_5 : MeasureTheory.SMulInvariantMeasure G α μ] [inst_6 : Countable G], MeasureTheory.IsFundamentalDomain G s μ → ∀ (f : α → ENNReal) (t : Set α), ∫⁻ (x : α) in t, f x ∂μ = ∑' (g : G), ∫⁻ (x : α) in g • t ∩ s, f (g⁻¹ • x) ∂μ - MeasureTheory.IsAddFundamentalDomain.measure_set_eq Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s t : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableVAdd G α] [inst_5 : MeasureTheory.VAddInvariantMeasure G α μ] [inst_6 : Countable G], MeasureTheory.IsAddFundamentalDomain G s μ → MeasureTheory.IsAddFundamentalDomain G t μ → ∀ {A : Set α}, MeasurableSet A → (∀ (g : G), (fun x => g +ᵥ x) ⁻¹' A = A) → μ (A ∩ s) = μ (A ∩ t) - MeasureTheory.IsFundamentalDomain.measure_set_eq Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s t : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableSMul G α] [inst_5 : MeasureTheory.SMulInvariantMeasure G α μ] [inst_6 : Countable G], MeasureTheory.IsFundamentalDomain G s μ → MeasureTheory.IsFundamentalDomain G t μ → ∀ {A : Set α}, MeasurableSet A → (∀ (g : G), (fun x => g • x) ⁻¹' A = A) → μ (A ∩ s) = μ (A ∩ t) - MeasureTheory.IsAddFundamentalDomain.addQuotientMeasure_eq Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] (μ : MeasureTheory.Measure α) [inst_3 : Countable G] [inst_4 : MeasurableSpace G] {s t : Set α} [inst_5 : MeasureTheory.VAddInvariantMeasure G α μ] [inst_6 : MeasurableVAdd G α], MeasureTheory.IsAddFundamentalDomain G s μ → MeasureTheory.IsAddFundamentalDomain G t μ → MeasureTheory.Measure.map (Quotient.mk (AddAction.orbitRel G α)) (μ.restrict s) = MeasureTheory.Measure.map (Quotient.mk (AddAction.orbitRel G α)) (μ.restrict t) - MeasureTheory.IsFundamentalDomain.quotientMeasure_eq Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] (μ : MeasureTheory.Measure α) [inst_3 : Countable G] [inst_4 : MeasurableSpace G] {s t : Set α} [inst_5 : MeasureTheory.SMulInvariantMeasure G α μ] [inst_6 : MeasurableSMul G α], MeasureTheory.IsFundamentalDomain G s μ → MeasureTheory.IsFundamentalDomain G t μ → MeasureTheory.Measure.map (Quotient.mk (MulAction.orbitRel G α)) (μ.restrict s) = MeasureTheory.Measure.map (Quotient.mk (MulAction.orbitRel G α)) (μ.restrict t) - MeasureTheory.IsAddFundamentalDomain.addProjection_respects_measure_apply Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {ν : MeasureTheory.Measure α} (μ : MeasureTheory.Measure (Quotient (AddAction.orbitRel G α))) [i : MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ] {t : Set α}, MeasureTheory.IsAddFundamentalDomain G t ν → ∀ {U : Set (Quotient (AddAction.orbitRel G α))}, MeasurableSet U → μ U = ν (Quotient.mk (AddAction.orbitRel G α) ⁻¹' U ∩ t) - MeasureTheory.IsFundamentalDomain.projection_respects_measure_apply Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {ν : MeasureTheory.Measure α} (μ : MeasureTheory.Measure (Quotient (MulAction.orbitRel G α))) [i : MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ] {t : Set α}, MeasureTheory.IsFundamentalDomain G t ν → ∀ {U : Set (Quotient (MulAction.orbitRel G α))}, MeasurableSet U → μ U = ν (Quotient.mk (MulAction.orbitRel G α) ⁻¹' U ∩ t) - MeasureTheory.IsAddFundamentalDomain.image_of_equiv Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {H : Type u_2} {α : Type u_3} {β : Type u_4} [inst : AddGroup G] [inst_1 : AddGroup H] [inst_2 : AddAction G α] [inst_3 : MeasurableSpace α] [inst_4 : AddAction H β] [inst_5 : MeasurableSpace β] {s : Set α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β}, MeasureTheory.IsAddFundamentalDomain G s μ → ∀ (f : α ≃ β), MeasureTheory.Measure.QuasiMeasurePreserving (⇑f.symm) ν μ → ∀ (e : H ≃ G), (∀ (g : H), Function.Semiconj (⇑f) (fun x => e g +ᵥ x) fun x => g +ᵥ x) → MeasureTheory.IsAddFundamentalDomain H (⇑f '' s) ν - MeasureTheory.IsFundamentalDomain.image_of_equiv Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {H : Type u_2} {α : Type u_3} {β : Type u_4} [inst : Group G] [inst_1 : Group H] [inst_2 : MulAction G α] [inst_3 : MeasurableSpace α] [inst_4 : MulAction H β] [inst_5 : MeasurableSpace β] {s : Set α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β}, MeasureTheory.IsFundamentalDomain G s μ → ∀ (f : α ≃ β), MeasureTheory.Measure.QuasiMeasurePreserving (⇑f.symm) ν μ → ∀ (e : H ≃ G), (∀ (g : H), Function.Semiconj (⇑f) (fun x => e g • x) fun x => g • x) → MeasureTheory.IsFundamentalDomain H (⇑f '' s) ν - MeasureTheory.IsAddFundamentalDomain.exists_ne_zero_vadd_eq Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s t : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableVAdd G α] [inst_5 : MeasureTheory.VAddInvariantMeasure G α μ] [inst_6 : Countable G], MeasureTheory.IsAddFundamentalDomain G s μ → MeasureTheory.NullMeasurableSet t μ → μ s < μ t → ∃ x ∈ t, ∃ y ∈ t, ∃ g, g ≠ 0 ∧ g +ᵥ x = y - MeasureTheory.IsFundamentalDomain.exists_ne_one_smul_eq Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s t : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableSMul G α] [inst_5 : MeasureTheory.SMulInvariantMeasure G α μ] [inst_6 : Countable G], MeasureTheory.IsFundamentalDomain G s μ → MeasureTheory.NullMeasurableSet t μ → μ s < μ t → ∃ x ∈ t, ∃ y ∈ t, ∃ g, g ≠ 1 ∧ g • x = y - MeasureTheory.IsAddFundamentalDomain.setIntegral_eq_tsum' Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} {E : Type u_5} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] [inst_3 : NormedAddCommGroup E] {s : Set α} {μ : MeasureTheory.Measure α} [inst_4 : MeasurableSpace G] [inst_5 : MeasurableVAdd G α] [inst_6 : MeasureTheory.VAddInvariantMeasure G α μ] [inst_7 : Countable G] [inst_8 : NormedSpace ℝ E], MeasureTheory.IsAddFundamentalDomain G s μ → ∀ {f : α → E} {t : Set α}, MeasureTheory.IntegrableOn f t μ → ∫ (x : α) in t, f x ∂μ = ∑' (g : G), ∫ (x : α) in (g +ᵥ t) ∩ s, f (-g +ᵥ x) ∂μ - MeasureTheory.IsFundamentalDomain.setIntegral_eq_tsum' Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} {E : Type u_5} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] [inst_3 : NormedAddCommGroup E] {s : Set α} {μ : MeasureTheory.Measure α} [inst_4 : MeasurableSpace G] [inst_5 : MeasurableSMul G α] [inst_6 : MeasureTheory.SMulInvariantMeasure G α μ] [inst_7 : Countable G] [inst_8 : NormedSpace ℝ E], MeasureTheory.IsFundamentalDomain G s μ → ∀ {f : α → E} {t : Set α}, MeasureTheory.IntegrableOn f t μ → ∫ (x : α) in t, f x ∂μ = ∑' (g : G), ∫ (x : α) in g • t ∩ s, f (g⁻¹ • x) ∂μ - MeasureTheory.IsFundamentalDomain.set_integral_eq_tsum' Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} {E : Type u_5} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] [inst_3 : NormedAddCommGroup E] {s : Set α} {μ : MeasureTheory.Measure α} [inst_4 : MeasurableSpace G] [inst_5 : MeasurableSMul G α] [inst_6 : MeasureTheory.SMulInvariantMeasure G α μ] [inst_7 : Countable G] [inst_8 : NormedSpace ℝ E], MeasureTheory.IsFundamentalDomain G s μ → ∀ {f : α → E} {t : Set α}, MeasureTheory.IntegrableOn f t μ → ∫ (x : α) in t, f x ∂μ = ∑' (g : G), ∫ (x : α) in g • t ∩ s, f (g⁻¹ • x) ∂μ - MeasureTheory.IsAddFundamentalDomain.mk_of_measure_univ_le Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasureTheory.IsFiniteMeasure μ] [inst_4 : Countable G], MeasureTheory.NullMeasurableSet s μ → (∀ (g : G), g ≠ 0 → MeasureTheory.AEDisjoint μ (g +ᵥ s) s) → (∀ (g : G), MeasureTheory.Measure.QuasiMeasurePreserving (fun x => g +ᵥ x) μ μ) → μ Set.univ ≤ ∑' (g : G), μ (g +ᵥ s) → MeasureTheory.IsAddFundamentalDomain G s μ - MeasureTheory.IsFundamentalDomain.mk_of_measure_univ_le Mathlib.MeasureTheory.Group.FundamentalDomain
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasureTheory.IsFiniteMeasure μ] [inst_4 : Countable G], MeasureTheory.NullMeasurableSet s μ → (∀ (g : G), g ≠ 1 → MeasureTheory.AEDisjoint μ (g • s) s) → (∀ (g : G), MeasureTheory.Measure.QuasiMeasurePreserving (fun x => g • x) μ μ) → μ Set.univ ≤ ∑' (g : G), μ (g • s) → MeasureTheory.IsFundamentalDomain G s μ - Zspan.fundamentalDomain Mathlib.Algebra.Module.Zlattice.Basic
{E : Type u_1} → {ι : Type u_2} → {K : Type u_3} → [inst : NormedLinearOrderedField K] → [inst_1 : NormedAddCommGroup E] → [inst_2 : NormedSpace K E] → Basis ι K E → Set E - Zspan.fundamentalDomain_measurableSet Mathlib.Algebra.Module.Zlattice.Basic
∀ {E : Type u_1} {ι : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (b : Basis ι ℝ E) [inst_2 : MeasurableSpace E] [inst_3 : OpensMeasurableSpace E] [inst_4 : Finite ι], MeasurableSet (Zspan.fundamentalDomain b) - Zspan.fundamentalDomain_pi_basisFun Mathlib.Algebra.Module.Zlattice.Basic
∀ {ι : Type u_2} [inst : Fintype ι], Zspan.fundamentalDomain (Pi.basisFun ℝ ι) = Set.univ.pi fun x => Set.Ico 0 1 - Zspan.fract_mem_fundamentalDomain Mathlib.Algebra.Module.Zlattice.Basic
∀ {E : Type u_1} {ι : Type u_2} {K : Type u_3} [inst : NormedLinearOrderedField K] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace K E] (b : Basis ι K E) [inst_3 : FloorRing K] [inst_4 : Fintype ι] (x : E), Zspan.fract b x ∈ Zspan.fundamentalDomain b - Zspan.measure_fundamentalDomain_ne_zero Mathlib.Algebra.Module.Zlattice.Basic
∀ {E : Type u_1} {ι : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (b : Basis ι ℝ E) [inst_2 : Finite ι] [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] {μ : MeasureTheory.Measure E} [inst_5 : μ.IsAddHaarMeasure], μ (Zspan.fundamentalDomain b) ≠ 0 - Zspan.fundamentalDomain_isBounded Mathlib.Algebra.Module.Zlattice.Basic
∀ {E : Type u_1} {ι : Type u_2} {K : Type u_3} [inst : NormedLinearOrderedField K] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace K E] (b : Basis ι K E) [inst_3 : FloorRing K] [inst_4 : Finite ι] [inst_5 : HasSolidNorm K], Bornology.IsBounded (Zspan.fundamentalDomain b) - Zspan.fundamentalDomain_subset_parallelepiped Mathlib.Algebra.Module.Zlattice.Basic
∀ {E : Type u_1} {ι : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (b : Basis ι ℝ E) [inst_2 : Fintype ι], Zspan.fundamentalDomain b ⊆ parallelepiped ⇑b - Zspan.fundamentalDomain_reindex Mathlib.Algebra.Module.Zlattice.Basic
∀ {E : Type u_1} {ι : Type u_2} {K : Type u_3} [inst : NormedLinearOrderedField K] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace K E] (b : Basis ι K E) {ι' : Type u_4} (e : ι ≃ ι'), Zspan.fundamentalDomain (b.reindex e) = Zspan.fundamentalDomain b - Zspan.fundamentalDomain_ae_parallelepiped Mathlib.Algebra.Module.Zlattice.Basic
∀ {E : Type u_1} {ι : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (b : Basis ι ℝ E) [inst_2 : Fintype ι] [inst_3 : MeasurableSpace E] (μ : MeasureTheory.Measure E) [inst_4 : BorelSpace E] [inst_5 : μ.IsAddHaarMeasure], μ.ae.EventuallyEq (Zspan.fundamentalDomain b) (parallelepiped ⇑b) - Zspan.volume_fundamentalDomain Mathlib.Algebra.Module.Zlattice.Basic
∀ {ι : Type u_2} [inst : Fintype ι] [inst_1 : DecidableEq ι] (b : Basis ι ℝ (ι → ℝ)), MeasureTheory.volume (Zspan.fundamentalDomain b) = ENNReal.ofReal |(Matrix.of ⇑b).det| - Zspan.measure_fundamentalDomain Mathlib.Algebra.Module.Zlattice.Basic
∀ {E : Type u_1} {ι : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (b : Basis ι ℝ E) [inst_2 : Fintype ι] [inst_3 : DecidableEq ι] [inst_4 : MeasurableSpace E] (μ : MeasureTheory.Measure E) [inst_5 : BorelSpace E] [inst_6 : μ.IsAddHaarMeasure] (b₀ : Basis ι ℝ E), μ (Zspan.fundamentalDomain b) = ENNReal.ofReal |b₀.det ⇑b| * μ (Zspan.fundamentalDomain b₀) - Zlattice.isAddFundamentalDomain Mathlib.Algebra.Module.Zlattice.Basic
∀ {ι : Type u_3} {E : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E] {L : AddSubgroup E} [inst_3 : DiscreteTopology ↥L] [inst_4 : IsZlattice ℝ L] [inst_5 : Finite ι] (b : Basis ι ℤ ↥L) [inst_6 : MeasurableSpace E] [inst_7 : OpensMeasurableSpace E] (μ : MeasureTheory.Measure E), MeasureTheory.IsAddFundamentalDomain (↥L) (Zspan.fundamentalDomain (Basis.ofZlatticeBasis ℝ L b)) μ - Zspan.isAddFundamentalDomain Mathlib.Algebra.Module.Zlattice.Basic
∀ {E : Type u_1} {ι : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (b : Basis ι ℝ E) [inst_2 : Finite ι] [inst_3 : MeasurableSpace E] [inst_4 : OpensMeasurableSpace E] (μ : MeasureTheory.Measure E), MeasureTheory.IsAddFundamentalDomain (↥(Submodule.span ℤ (Set.range ⇑b)).toAddSubgroup) (Zspan.fundamentalDomain b) μ - Zspan.map_fundamentalDomain Mathlib.Algebra.Module.Zlattice.Basic
∀ {E : Type u_1} {ι : Type u_2} {K : Type u_3} [inst : NormedLinearOrderedField K] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace K E] (b : Basis ι K E) {F : Type u_4} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace K F] (f : E ≃ₗ[K] F), ⇑f '' Zspan.fundamentalDomain b = Zspan.fundamentalDomain (b.map f) - Zspan.fundamentalDomain.eq_1 Mathlib.Algebra.Module.Zlattice.Basic
∀ {E : Type u_1} {ι : Type u_2} {K : Type u_3} [inst : NormedLinearOrderedField K] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace K E] (b : Basis ι K E), Zspan.fundamentalDomain b = {m | ∀ (i : ι), (b.repr m) i ∈ Set.Ico 0 1} - Zspan.mem_fundamentalDomain Mathlib.Algebra.Module.Zlattice.Basic
∀ {E : Type u_1} {ι : Type u_2} {K : Type u_3} [inst : NormedLinearOrderedField K] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace K E] (b : Basis ι K E) {m : E}, m ∈ Zspan.fundamentalDomain b ↔ ∀ (i : ι), (b.repr m) i ∈ Set.Ico 0 1 - Zspan.exist_unique_vadd_mem_fundamentalDomain Mathlib.Algebra.Module.Zlattice.Basic
∀ {E : Type u_1} {ι : Type u_2} {K : Type u_3} [inst : NormedLinearOrderedField K] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace K E] (b : Basis ι K E) [inst_3 : FloorRing K] [inst_4 : Finite ι] (x : E), ∃! v, v +ᵥ x ∈ Zspan.fundamentalDomain b - Zspan.vadd_mem_fundamentalDomain Mathlib.Algebra.Module.Zlattice.Basic
∀ {E : Type u_1} {ι : Type u_2} {K : Type u_3} [inst : NormedLinearOrderedField K] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace K E] (b : Basis ι K E) [inst_3 : FloorRing K] [inst_4 : Fintype ι] (y : ↥(Submodule.span ℤ (Set.range ⇑b))) (x : E), y +ᵥ x ∈ Zspan.fundamentalDomain b ↔ y = -Zspan.floor b x - Zlattice.covolume_eq_measure_fundamentalDomain Mathlib.Algebra.Module.Zlattice.Covolume
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E] [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] (L : AddSubgroup E) [inst_5 : DiscreteTopology ↥L] [inst_6 : IsZlattice ℝ L] (μ : autoParam (MeasureTheory.Measure E) _auto✝) [inst_7 : MeasureTheory.Measure.IsAddHaarMeasure μ] {F : Set E}, MeasureTheory.IsAddFundamentalDomain (↥L) F μ → Zlattice.covolume L μ = (μ F).toReal - FundamentalGroupoid.termπ Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Lean.ParserDescr - FundamentalGroupoid.termπₓ Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Lean.ParserDescr - FundamentalGroupoid.termπₘ Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Lean.ParserDescr - FundamentalGroupoid Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Type u → Type u - FundamentalGroupoid.as Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
{X : Type u} → FundamentalGroupoid X → X - FundamentalGroupoid.mk Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
{X : Type u} → X → FundamentalGroupoid X
Did you maybe mean
About
Loogle searches of Lean and Mathlib definitions and theorems.
You may also want to try the CLI version, the VS
Code extension, the lean.nvim
integration or the Zulip bot.
Usage
Loogle finds definitions and lemmas in various ways:
By constant:
🔍Real.sin
finds all lemmas whose statement somehow mentions the sine function.By lemma name substring:
🔍"differ"
finds all lemmas that have"differ"
somewhere in their lemma name.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
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 findtsum_lt_tsum
even though the hypothesisf i < g i
is not the last.
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, _ * _, _ ^ _, |- _ < _ → _
woould 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 currently provided by Joachim Breitner <mail@joachim-breitner.de>.
This is Loogle revision fa2ddf5
serving mathlib revision d874bdf