Theorems · Theorem · combinatorics

Sym2.lift_map_apply

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : γ → α} (f : { f // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }) (p : Sym2 γ),
  Sym2.lift f (Sym2.map g p) = Sym2.lift ⟨fun c₁ c₂ => ↑f (g c₁) (g c₂), ⋯⟩ p

Defined in

Mathlib.Data.Sym.Sym2

Cited by

0 results in Mathlib

Foundations

Depth 18 from the axioms · uses propext, Classical.choice, Quot.sound