Loogle!

Result

Found 73 declarations mentioning Sum.map.

Sum.map 📋 Init.Data.Sum.Basic
{α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} (f : α → α') (g : β → β') : α ⊕ β → α' ⊕ β'
Sum.map_inl 📋 Init.Data.Sum.Basic
{α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} (f : α → α') (g : β → β') (x : α) : Sum.map f g (Sum.inl x) = Sum.inl (f x)
Sum.map_inr 📋 Init.Data.Sum.Basic
{α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} (f : α → α') (g : β → β') (x : β) : Sum.map f g (Sum.inr x) = Sum.inr (g x)
Sum.map_id_id 📋 Init.Data.Sum.Lemmas
{α : Type u_1} {β : Type u_2} : Sum.map id id = id
Sum.isLeft_map 📋 Init.Data.Sum.Lemmas
{α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β) (g : γ → δ) (x : α ⊕ γ) : (Sum.map f g x).isLeft = x.isLeft
Sum.isRight_map 📋 Init.Data.Sum.Lemmas
{α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β) (g : γ → δ) (x : α ⊕ γ) : (Sum.map f g x).isRight = x.isRight
Sum.getLeft?_map 📋 Init.Data.Sum.Lemmas
{α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β) (g : γ → δ) (x : α ⊕ γ) : (Sum.map f g x).getLeft? = Option.map f x.getLeft?
Sum.getRight?_map 📋 Init.Data.Sum.Lemmas
{α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β) (g : γ → δ) (x : α ⊕ γ) : (Sum.map f g x).getRight? = Option.map g x.getRight?
Sum.elim_map 📋 Init.Data.Sum.Lemmas
{α : Type u_1} {β : Type u_2} {ε : Sort u_3} {γ : Type u_4} {δ : Type u_5} {f₁ : α → β} {f₂ : β → ε} {g₁ : γ → δ} {g₂ : δ → ε} {x : α ⊕ γ} : Sum.elim f₂ g₂ (Sum.map f₁ g₁ x) = Sum.elim (f₂ ∘ f₁) (g₂ ∘ g₁) x
Sum.map_map 📋 Init.Data.Sum.Lemmas
{α' : Type u_1} {α'' : Type u_2} {β' : Type u_3} {β'' : Type u_4} {α : Type u_5} {β : Type u_6} (f' : α' → α'') (g' : β' → β'') (f : α → α') (g : β → β') (x : α ⊕ β) : Sum.map f' g' (Sum.map f g x) = Sum.map (f' ∘ f) (g' ∘ g) x
Sum.elim_comp_map 📋 Init.Data.Sum.Lemmas
{α : Type u_1} {β : Type u_2} {ε : Sort u_3} {γ : Type u_4} {δ : Type u_5} {f₁ : α → β} {f₂ : β → ε} {g₁ : γ → δ} {g₂ : δ → ε} : Sum.elim f₂ g₂ ∘ Sum.map f₁ g₁ = Sum.elim (f₂ ∘ f₁) (g₂ ∘ g₁)
Sum.map_comp_map 📋 Init.Data.Sum.Lemmas
{α' : Type u_1} {α'' : Type u_2} {β' : Type u_3} {β'' : Type u_4} {α : Type u_5} {β : Type u_6} (f' : α' → α'') (g' : β' → β'') (f : α → α') (g : β → β') : Sum.map f' g' ∘ Sum.map f g = Sum.map (f' ∘ f) (g' ∘ g)
Function.Bijective.sumMap 📋 Mathlib.Data.Sum.Basic
{α : Type u} {α' : Type w} {β : Type v} {β' : Type x} {f : α → β} {g : α' → β'} (hf : Function.Bijective f) (hg : Function.Bijective g) : Function.Bijective (Sum.map f g)
Function.Bijective.sum_map 📋 Mathlib.Data.Sum.Basic
{α : Type u} {α' : Type w} {β : Type v} {β' : Type x} {f : α → β} {g : α' → β'} (hf : Function.Bijective f) (hg : Function.Bijective g) : Function.Bijective (Sum.map f g)
Function.Injective.sumMap 📋 Mathlib.Data.Sum.Basic
{α : Type u} {α' : Type w} {β : Type v} {β' : Type x} {f : α → β} {g : α' → β'} (hf : Function.Injective f) (hg : Function.Injective g) : Function.Injective (Sum.map f g)
Function.Injective.sum_map 📋 Mathlib.Data.Sum.Basic
{α : Type u} {α' : Type w} {β : Type v} {β' : Type x} {f : α → β} {g : α' → β'} (hf : Function.Injective f) (hg : Function.Injective g) : Function.Injective (Sum.map f g)
Function.Surjective.sumMap 📋 Mathlib.Data.Sum.Basic
{α : Type u} {α' : Type w} {β : Type v} {β' : Type x} {f : α → β} {g : α' → β'} (hf : Function.Surjective f) (hg : Function.Surjective g) : Function.Surjective (Sum.map f g)
Function.Surjective.sum_map 📋 Mathlib.Data.Sum.Basic
{α : Type u} {α' : Type w} {β : Type v} {β' : Type x} {f : α → β} {g : α' → β'} (hf : Function.Surjective f) (hg : Function.Surjective g) : Function.Surjective (Sum.map f g)
Sum.map_bijective 📋 Mathlib.Data.Sum.Basic
{α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {f : α → γ} {g : β → δ} : Function.Bijective (Sum.map f g) ↔ Function.Bijective f ∧ Function.Bijective g
Sum.map_injective 📋 Mathlib.Data.Sum.Basic
{α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {f : α → γ} {g : β → δ} : Function.Injective (Sum.map f g) ↔ Function.Injective f ∧ Function.Injective g
Sum.map_surjective 📋 Mathlib.Data.Sum.Basic
{α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {f : α → γ} {g : β → δ} : Function.Surjective (Sum.map f g) ↔ Function.Surjective f ∧ Function.Surjective g
Equiv.Perm.sumCongr_apply 📋 Mathlib.Logic.Equiv.Sum
{α : Type u_9} {β : Type u_10} (ea : Equiv.Perm α) (eb : Equiv.Perm β) (x : α ⊕ β) : (ea.sumCongr eb) x = Sum.map (⇑ea) (⇑eb) x
Equiv.sumCongr_apply 📋 Mathlib.Logic.Equiv.Sum
{α₁ : Type u_9} {α₂ : Type u_10} {β₁ : Type u_11} {β₂ : Type u_12} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) (a✝ : α₁ ⊕ β₁) : (ea.sumCongr eb) a✝ = Sum.map (⇑ea) (⇑eb) a✝
Equiv.sigmaSumDistrib_apply 📋 Mathlib.Logic.Equiv.Sum
{ι : Type u_11} (α : ι → Type u_9) (β : ι → Type u_10) (p : (i : ι) × (α i ⊕ β i)) : (Equiv.sigmaSumDistrib α β) p = Sum.map (Sigma.mk p.fst) (Sigma.mk p.fst) p.snd
Equiv.sumSumSumComm_apply 📋 Mathlib.Logic.Equiv.Sum
(α : Type u_9) (β : Type u_10) (γ : Type u_11) (δ : Type u_12) (a✝ : (α ⊕ β) ⊕ γ ⊕ δ) : (Equiv.sumSumSumComm α β γ δ) a✝ = (⇑(Equiv.sumAssoc (α ⊕ γ) β δ) ∘ Sum.map (⇑(Equiv.sumAssoc α γ β).symm) id ∘ Sum.map (Sum.map id ⇑(Equiv.sumComm β γ)) id ∘ Sum.map (⇑(Equiv.sumAssoc α β γ)) id ∘ ⇑(Equiv.sumAssoc (α ⊕ β) γ δ).symm) a✝
Sum.map.eq_1 📋 Mathlib.Logic.Equiv.Basic
{α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} (f : α → α') (g : β → β') : Sum.map f g = Sum.elim (Sum.inl ∘ f) (Sum.inr ∘ g)
Function.Embedding.coe_sumMap 📋 Mathlib.Logic.Embedding.Basic
{α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e₁ : α ↪ β) (e₂ : γ ↪ δ) : ⇑(e₁.sumMap e₂) = Sum.map ⇑e₁ ⇑e₂
RelEmbedding.sumLexMap_apply 📋 Mathlib.Order.RelIso.Basic
{α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} {u : δ → δ → Prop} (f : r ↪r s) (g : t ↪r u) (a✝ : α ⊕ γ) : (f.sumLexMap g) a✝ = Sum.map (⇑f) (⇑g) a✝
RelEmbedding.sumLiftRelMap_apply 📋 Mathlib.Order.RelIso.Basic
{α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} {u : δ → δ → Prop} (f : r ↪r s) (g : t ↪r u) (a✝ : α ⊕ γ) : (f.sumLiftRelMap g) a✝ = Sum.map (⇑f) (⇑g) a✝
Prefunctor.symmetrify_map 📋 Mathlib.Combinatorics.Quiver.Symmetric
{U : Type u_1} {V : Type u_2} [Quiver U] [Quiver V] (φ : U ⥤q V) {X✝ Y✝ : Quiver.Symmetrify U} (a✝ : (X✝ ⟶ Y✝) ⊕ (Y✝ ⟶ X✝)) : φ.symmetrify.map a✝ = Sum.map φ.map φ.map a✝
Continuous.sumMap 📋 Mathlib.Topology.Constructions.SumProd
{X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace W] [TopologicalSpace Z] {f : X → Y} {g : Z → W} (hf : Continuous f) (hg : Continuous g) : Continuous (Sum.map f g)
Continuous.sum_map 📋 Mathlib.Topology.Constructions.SumProd
{X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace W] [TopologicalSpace Z] {f : X → Y} {g : Z → W} (hf : Continuous f) (hg : Continuous g) : Continuous (Sum.map f g)
IsClosedMap.sumMap 📋 Mathlib.Topology.Constructions.SumProd
{X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace W] [TopologicalSpace Z] {f : X → Y} {g : Z → W} (hf : IsClosedMap f) (hg : IsClosedMap g) : IsClosedMap (Sum.map f g)
IsOpenMap.sumMap 📋 Mathlib.Topology.Constructions.SumProd
{X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace W] [TopologicalSpace Z] {f : X → Y} {g : Z → W} (hf : IsOpenMap f) (hg : IsOpenMap g) : IsOpenMap (Sum.map f g)
continuous_sumMap 📋 Mathlib.Topology.Constructions.SumProd
{X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace W] [TopologicalSpace Z] {f : X → Y} {g : Z → W} : Continuous (Sum.map f g) ↔ Continuous f ∧ Continuous g
continuous_sum_map 📋 Mathlib.Topology.Constructions.SumProd
{X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace W] [TopologicalSpace Z] {f : X → Y} {g : Z → W} : Continuous (Sum.map f g) ↔ Continuous f ∧ Continuous g
IsHomeomorph.sumMap 📋 Mathlib.Topology.Homeomorph.Lemmas
{X : Type u_1} {Y : Type u_2} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {W : Type u_5} [TopologicalSpace W] {f : X → Y} {g : Z → W} (hf : IsHomeomorph f) (hg : IsHomeomorph g) : IsHomeomorph (Sum.map f g)
Sum.hasVAdd.eq_1 📋 Mathlib.Algebra.Group.Action.Sum
{M : Type u_1} {α : Type u_3} {β : Type u_4} [VAdd M α] [VAdd M β] : Sum.hasVAdd = { vadd := fun a => Sum.map (fun x => a +ᵥ x) fun x => a +ᵥ x }
Sum.instSMul.eq_1 📋 Mathlib.Algebra.Group.Action.Sum
{M : Type u_1} {α : Type u_3} {β : Type u_4} [SMul M α] [SMul M β] : Sum.instSMul = { smul := fun a => Sum.map (fun x => a • x) fun x => a • x }
Sum.smul_def 📋 Mathlib.Algebra.Group.Action.Sum
{M : Type u_1} {α : Type u_3} {β : Type u_4} [SMul M α] [SMul M β] (a : M) (x : α ⊕ β) : a • x = Sum.map (fun x => a • x) (fun x => a • x) x
Sum.vadd_def 📋 Mathlib.Algebra.Group.Action.Sum
{M : Type u_1} {α : Type u_3} {β : Type u_4} [VAdd M α] [VAdd M β] (a : M) (x : α ⊕ β) : a +ᵥ x = Sum.map (fun x => a +ᵥ x) (fun x => a +ᵥ x) x
Measurable.sumMap 📋 Mathlib.MeasureTheory.MeasurableSpace.Constructions
{α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x✝ : MeasurableSpace γ} {x✝¹ : MeasurableSpace δ} {f : α → β} {g : γ → δ} (hf : Measurable f) (hg : Measurable g) : Measurable (Sum.map f g)
ContMDiff.sumMap 📋 Mathlib.Geometry.Manifold.ContMDiff.Constructions
{𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_16} [TopologicalSpace M'] [ChartedSpace H M'] {n : WithTop ℕ∞} {E' : Type u_17} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_18} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 E' H'} {N : Type u_20} {N' : Type u_21} [TopologicalSpace N] [TopologicalSpace N'] [ChartedSpace H' N] [ChartedSpace H' N'] {f : M → N} {g : M' → N'} (hf : ContMDiff I J n f) (hg : ContMDiff I J n g) : ContMDiff I J n (Sum.map f g)
ContMDiff.sum_map 📋 Mathlib.Geometry.Manifold.ContMDiff.Constructions
{𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_16} [TopologicalSpace M'] [ChartedSpace H M'] {n : WithTop ℕ∞} {E' : Type u_17} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_18} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 E' H'} {N : Type u_20} {N' : Type u_21} [TopologicalSpace N] [TopologicalSpace N'] [ChartedSpace H' N] [ChartedSpace H' N'] {f : M → N} {g : M' → N'} (hf : ContMDiff I J n f) (hg : ContMDiff I J n g) : ContMDiff I J n (Sum.map f g)
contMDiff_sum_map 📋 Mathlib.Geometry.Manifold.ContMDiff.Constructions
{𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_16} [TopologicalSpace M'] [ChartedSpace H M'] {n : WithTop ℕ∞} {E' : Type u_17} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_18} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 E' H'} {N : Type u_20} {N' : Type u_21} [TopologicalSpace N] [TopologicalSpace N'] [ChartedSpace H' N] [ChartedSpace H' N'] {f : M → N} {g : M' → N'} : ContMDiff I J n (Sum.map f g) ↔ ContMDiff I J n f ∧ ContMDiff I J n g
Combinatorics.Subspace.reindex.eq_1 📋 Mathlib.Combinatorics.HalesJewett
{η : Type u_5} {α : Type u_6} {ι : Type u_7} {η' : Type u_9} {α' : Type u_10} {ι' : Type u_11} (l : Combinatorics.Subspace η α ι) (eη : η ≃ η') (eα : α ≃ α') (eι : ι ≃ ι') : l.reindex eη eα eι = { idxFun := fun i => Sum.map (⇑eα) (⇑eη) (l.idxFun (eι.symm i)), proper := ⋯ }
Prefunctor.symmetrifyCostar 📋 Mathlib.Combinatorics.Quiver.Covering
{U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) (u : U) : φ.symmetrify.costar u = ⇑(Quiver.symmetrifyCostar (φ.obj u)).symm ∘ Sum.map (φ.costar u) (φ.star u) ∘ ⇑(Quiver.symmetrifyCostar u)
Prefunctor.symmetrifyStar 📋 Mathlib.Combinatorics.Quiver.Covering
{U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) (u : U) : φ.symmetrify.star u = ⇑(Quiver.symmetrifyStar (φ.obj u)).symm ∘ Sum.map (φ.star u) (φ.costar u) ∘ ⇑(Quiver.symmetrifyStar u)
FirstOrder.Language.LHom.sumMap_onFunction 📋 Mathlib.ModelTheory.LanguageMap
{L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') {L₁ : FirstOrder.Language} {L₂ : FirstOrder.Language} (ψ : L₁ →ᴸ L₂) (_n : ℕ) (a✝ : L.Functions _n ⊕ L₁.Functions _n) : (ϕ.sumMap ψ).onFunction a✝ = Sum.map (fun f => ϕ.onFunction f) (fun f => ψ.onFunction f) a✝
FirstOrder.Language.LHom.sumMap_onRelation 📋 Mathlib.ModelTheory.LanguageMap
{L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') {L₁ : FirstOrder.Language} {L₂ : FirstOrder.Language} (ψ : L₁ →ᴸ L₂) (_n : ℕ) (a✝ : L.Relations _n ⊕ L₁.Relations _n) : (ϕ.sumMap ψ).onRelation a✝ = Sum.map (fun f => ϕ.onRelation f) (fun f => ψ.onRelation f) a✝
FirstOrder.Language.BoundedFormula.relabelAux_sumInl 📋 Mathlib.ModelTheory.Syntax
{α : Type u'} {n : ℕ} (k : ℕ) : FirstOrder.Language.BoundedFormula.relabelAux Sum.inl k = Sum.map id (Fin.natAdd n)
FirstOrder.Language.BoundedFormula.relabelAux_sum_inl 📋 Mathlib.ModelTheory.Syntax
{α : Type u'} {n : ℕ} (k : ℕ) : FirstOrder.Language.BoundedFormula.relabelAux Sum.inl k = Sum.map id (Fin.natAdd n)
FirstOrder.Language.BoundedFormula.castLE.eq_3 📋 Mathlib.ModelTheory.Syntax
{L : FirstOrder.Language} {α : Type u'} (x✝ x✝¹ : ℕ) (x✝² : x✝ ≤ x✝¹) (l : ℕ) (R : L.Relations l) (ts : Fin l → L.Term (α ⊕ Fin x✝)) : FirstOrder.Language.BoundedFormula.castLE x✝² (FirstOrder.Language.BoundedFormula.rel R ts) = FirstOrder.Language.BoundedFormula.rel R (FirstOrder.Language.Term.relabel (Sum.map id (Fin.castLE x✝²)) ∘ ts)
FirstOrder.Language.BoundedFormula.castLE.eq_2 📋 Mathlib.ModelTheory.Syntax
{L : FirstOrder.Language} {α : Type u'} (x✝ x✝¹ : ℕ) (x✝² : x✝ ≤ x✝¹) (t₁ t₂ : L.Term (α ⊕ Fin x✝)) : FirstOrder.Language.BoundedFormula.castLE x✝² (FirstOrder.Language.BoundedFormula.equal t₁ t₂) = FirstOrder.Language.BoundedFormula.equal (FirstOrder.Language.Term.relabel (Sum.map id (Fin.castLE x✝²)) t₁) (FirstOrder.Language.Term.relabel (Sum.map id (Fin.castLE x✝²)) t₂)
FirstOrder.Language.BoundedFormula.relabelAux.eq_1 📋 Mathlib.ModelTheory.Syntax
{α : Type u'} {β : Type v'} {n : ℕ} (g : α → β ⊕ Fin n) (k : ℕ) : FirstOrder.Language.BoundedFormula.relabelAux g k = Sum.map id ⇑finSumFinEquiv ∘ ⇑(Equiv.sumAssoc β (Fin n) (Fin k)) ∘ Sum.map g id
FirstOrder.Language.BoundedFormula.toFormula.eq_5 📋 Mathlib.ModelTheory.Syntax
{L : FirstOrder.Language} {α : Type u'} (x✝ : ℕ) (f : L.BoundedFormula α (x✝ + 1)) : f.all.toFormula = (FirstOrder.Language.BoundedFormula.relabel (Sum.elim (Sum.inl ∘ Sum.inl) (Sum.map Sum.inr id ∘ ⇑finSumFinEquiv.symm)) f.toFormula).all
FirstOrder.Language.Term.realize_liftAt 📋 Mathlib.ModelTheory.Semantics
{L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {n n' m : ℕ} {t : L.Term (α ⊕ Fin n)} {v : α ⊕ Fin (n + n') → M} : FirstOrder.Language.Term.realize v (FirstOrder.Language.Term.liftAt n' m t) = FirstOrder.Language.Term.realize (v ∘ Sum.map id fun i => if ↑i < m then Fin.castAdd n' i else i.addNat n') t
FirstOrder.Language.Formula.iAlls.eq_1 📋 Mathlib.ModelTheory.Semantics
{L : FirstOrder.Language} {α : Type u'} (β : Type v') [Finite β] (φ : L.Formula (α ⊕ β)) : FirstOrder.Language.Formula.iAlls β φ = (FirstOrder.Language.BoundedFormula.relabel (fun a => Sum.map id (⇑(Classical.choice ⋯)) a) φ).alls
FirstOrder.Language.Formula.iExs.eq_1 📋 Mathlib.ModelTheory.Semantics
{L : FirstOrder.Language} {α : Type u'} (β : Type v') [Finite β] (φ : L.Formula (α ⊕ β)) : FirstOrder.Language.Formula.iExs β φ = (FirstOrder.Language.BoundedFormula.relabel (fun a => Sum.map id (⇑(Classical.choice ⋯)) a) φ).exs
FirstOrder.genericPolyMapSurjOnOfInjOn.eq_1 📋 Mathlib.FieldTheory.AxGrothendieck
{ι : Type u_1} {α : Type u_2} [Finite α] [Finite ι] (φ : FirstOrder.Language.ring.Formula (α ⊕ ι)) (mons : ι → Finset (ι →₀ ℕ)) : FirstOrder.genericPolyMapSurjOnOfInjOn φ mons = FirstOrder.Language.Formula.iAlls (α ⊕ (i : ι) × { x // x ∈ mons i }) (FirstOrder.Language.Formula.relabel Sum.inr ((FirstOrder.Language.Formula.iAlls ι ((FirstOrder.Language.Formula.relabel (Sum.map Sum.inl id) φ).imp (FirstOrder.Language.BoundedFormula.subst φ (Sum.elim (fun a => FirstOrder.Language.var (Sum.inl (Sum.inl a))) fun i => FirstOrder.Language.Term.relabel (fun i => (Equiv.sumAssoc α ((i : ι) × { x // x ∈ mons i }) ι).symm (Sum.inr i)) (FirstOrder.Ring.termOfFreeCommRing (FirstOrder.Ring.genericPolyMap mons i)))))).imp ((FirstOrder.Language.Formula.iAlls (Fin 2 × ι) (FirstOrder.Language.BoundedFormula.imp (FirstOrder.Language.Formula.relabel (Sum.map Sum.inl fun i => (0, i)) φ) (FirstOrder.Language.BoundedFormula.imp (FirstOrder.Language.Formula.relabel (Sum.map Sum.inl fun i => (1, i)) φ) (FirstOrder.Language.Formula.relabel (fun x => (Equiv.sumAssoc α ((i : ι) × { x // x ∈ mons i }) (Fin 2 × ι)).symm (Sum.inr x)) (FirstOrder.Language.Formula.imp (FirstOrder.Language.BoundedFormula.iInf fun i => (FirstOrder.Language.Term.relabel (Sum.inl ∘ Sum.map id fun i => (0, i)) (FirstOrder.Ring.termOfFreeCommRing (FirstOrder.Ring.genericPolyMap mons i))).bdEqual (FirstOrder.Language.Term.relabel (Sum.inl ∘ Sum.map id fun i => (1, i)) (FirstOrder.Ring.termOfFreeCommRing (FirstOrder.Ring.genericPolyMap mons i)))) (FirstOrder.Language.BoundedFormula.iInf fun i => (FirstOrder.Language.var (Sum.inl (Sum.inr (0, i)))).bdEqual (FirstOrder.Language.var (Sum.inl (Sum.inr (1, i)))))))))).imp (FirstOrder.Language.Formula.iAlls ι ((FirstOrder.Language.Formula.relabel (Sum.map Sum.inl id) φ).imp (FirstOrder.Language.Formula.iExs ι (FirstOrder.Language.Formula.relabel (fun i => let_fun this := Sum.elim (Sum.inl ∘ Sum.inl) (fun i => if i.1 = 0 then Sum.inr i.2 else Sum.inl (Sum.inr i.2)) i; this) (FirstOrder.Language.Formula.relabel (Sum.map Sum.inl fun i => (0, i)) φ ⊓ FirstOrder.Language.Formula.relabel (fun x => (Equiv.sumAssoc α ((i : ι) × { x // x ∈ mons i }) (Fin 2 × ι)).symm (Sum.inr x)) (FirstOrder.Language.BoundedFormula.iInf fun i => (FirstOrder.Language.Term.relabel (Sum.inl ∘ Sum.map id fun i => (0, i)) (FirstOrder.Ring.termOfFreeCommRing (FirstOrder.Ring.genericPolyMap mons i))).bdEqual (FirstOrder.Language.var (Sum.inl (Sum.inr (1, i)))))))))))))
Diffeomorph.sumCongr_coe 📋 Mathlib.Geometry.Manifold.Diffeomorph
{𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} {M' : Type u_13} [TopologicalSpace M'] [ChartedSpace H M'] {N : Type u_15} [TopologicalSpace N] [ChartedSpace H N] {J : ModelWithCorners 𝕜 E' H} {N' : Type u_17} [TopologicalSpace N'] [ChartedSpace H N'] (φ : Diffeomorph I J M N n) (ψ : Diffeomorph I J M' N' n) : ⇑(φ.sumCongr ψ) = Sum.map ⇑φ ⇑ψ
AddMonoid.Coprod.map.eq_1 📋 Mathlib.GroupTheory.Coprod.Basic
{M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [AddZeroClass M] [AddZeroClass N] [AddZeroClass M'] [AddZeroClass N'] (f : M →+ M') (g : N →+ N') : AddMonoid.Coprod.map f g = AddMonoid.Coprod.clift (AddMonoid.Coprod.mk.comp (FreeAddMonoid.map (Sum.map ⇑f ⇑g))) ⋯ ⋯ ⋯ ⋯
Monoid.Coprod.map.eq_1 📋 Mathlib.GroupTheory.Coprod.Basic
{M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [MulOneClass M] [MulOneClass N] [MulOneClass M'] [MulOneClass N'] (f : M →* M') (g : N →* N') : Monoid.Coprod.map f g = Monoid.Coprod.clift (Monoid.Coprod.mk.comp (FreeMonoid.map (Sum.map ⇑f ⇑g))) ⋯ ⋯ ⋯ ⋯
AddMonoid.Coprod.instNeg.eq_1 📋 Mathlib.GroupTheory.Coprod.Basic
{G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] : AddMonoid.Coprod.instNeg = { neg := Quotient.map' (fun w => FreeAddMonoid.ofList (List.map (Sum.map Neg.neg Neg.neg) (FreeAddMonoid.toList w)).reverse) ⋯ }
Monoid.Coprod.instInv.eq_1 📋 Mathlib.GroupTheory.Coprod.Basic
{G : Type u_1} {H : Type u_2} [Group G] [Group H] : Monoid.Coprod.instInv = { inv := Quotient.map' (fun w => FreeMonoid.ofList (List.map (Sum.map Inv.inv Inv.inv) (FreeMonoid.toList w)).reverse) ⋯ }
AddMonoid.Coprod.con_neg_add_cancel 📋 Mathlib.GroupTheory.Coprod.Basic
{G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] (x : FreeAddMonoid (G ⊕ H)) : (AddMonoid.coprodCon G H) (FreeAddMonoid.ofList (List.map (Sum.map Neg.neg Neg.neg) (FreeAddMonoid.toList x)).reverse + x) 0
Monoid.Coprod.con_inv_mul_cancel 📋 Mathlib.GroupTheory.Coprod.Basic
{G : Type u_1} {H : Type u_2} [Group G] [Group H] (x : FreeMonoid (G ⊕ H)) : (Monoid.coprodCon G H) (FreeMonoid.ofList (List.map (Sum.map Inv.inv Inv.inv) (FreeMonoid.toList x)).reverse * x) 1
AddMonoid.Coprod.map_mk_ofList 📋 Mathlib.GroupTheory.Coprod.Basic
{M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [AddZeroClass M] [AddZeroClass N] [AddZeroClass M'] [AddZeroClass N'] (f : M →+ M') (g : N →+ N') (l : List (M ⊕ N)) : (AddMonoid.Coprod.map f g) (AddMonoid.Coprod.mk (FreeAddMonoid.ofList l)) = AddMonoid.Coprod.mk (FreeAddMonoid.ofList (List.map (Sum.map ⇑f ⇑g) l))
Monoid.Coprod.map_mk_ofList 📋 Mathlib.GroupTheory.Coprod.Basic
{M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [MulOneClass M] [MulOneClass N] [MulOneClass M'] [MulOneClass N'] (f : M →* M') (g : N →* N') (l : List (M ⊕ N)) : (Monoid.Coprod.map f g) (Monoid.Coprod.mk (FreeMonoid.ofList l)) = Monoid.Coprod.mk (FreeMonoid.ofList (List.map (Sum.map ⇑f ⇑g) l))
AddMonoid.Coprod.neg_def 📋 Mathlib.GroupTheory.Coprod.Basic
{G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] (w : FreeAddMonoid (G ⊕ H)) : -AddMonoid.Coprod.mk w = AddMonoid.Coprod.mk (FreeAddMonoid.ofList (List.map (Sum.map Neg.neg Neg.neg) (FreeAddMonoid.toList w)).reverse)
Monoid.Coprod.inv_def 📋 Mathlib.GroupTheory.Coprod.Basic
{G : Type u_1} {H : Type u_2} [Group G] [Group H] (w : FreeMonoid (G ⊕ H)) : (Monoid.Coprod.mk w)⁻¹ = Monoid.Coprod.mk (FreeMonoid.ofList (List.map (Sum.map Inv.inv Inv.inv) (FreeMonoid.toList w)).reverse)
AddMonoid.Coprod.mk_of_neg_add 📋 Mathlib.GroupTheory.Coprod.Basic
{G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] (x : G ⊕ H) : AddMonoid.Coprod.mk (FreeAddMonoid.of (Sum.map Neg.neg Neg.neg x)) + AddMonoid.Coprod.mk (FreeAddMonoid.of x) = 0
Monoid.Coprod.mk_of_inv_mul 📋 Mathlib.GroupTheory.Coprod.Basic
{G : Type u_1} {H : Type u_2} [Group G] [Group H] (x : G ⊕ H) : Monoid.Coprod.mk (FreeMonoid.of (Sum.map Inv.inv Inv.inv x)) * Monoid.Coprod.mk (FreeMonoid.of x) = 1

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. 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:

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 find tsum_lt_tsum even though the hypothesis f 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, _ * _, _ ^ _, |- _ < _ → _
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.

This is Loogle revision 19971e9 serving mathlib revision bce1d65