English
For all i ∈ Sym2 α, f i holds iff for all x,y, f(Sym2.mk (x,y)) holds.
Русский
Для каждого i ∈ Sym2 α верно f i тогда и только тогда, когда для всех x,y выполняется f(Sym2.mk (x,y)).
LaTeX
$$$$ \forall {\alpha} {f : Sym2 α \to Prop}, (\forall x:Sym2 α, f x) \iff (\forall x y, f (\mathrm{Sym2.mk}\{ fst := x, snd := y \})). $$$$
Lean4
/-- A two-argument version of `Sym2.lift`. -/
def lift₂ :
{ f : α → α → β → β → γ // ∀ a₁ a₂ b₁ b₂, f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ } ≃
(Sym2 α → Sym2 β → γ)
where
toFun
f :=
Quotient.lift₂ (s₁ := Sym2.Rel.setoid α) (s₂ := Sym2.Rel.setoid β)
(fun (a : α × α) (b : β × β) => f.1 a.1 a.2 b.1 b.2)
(by
rintro _ _ _ _ ⟨⟩ ⟨⟩
exacts [rfl, (f.2 _ _ _ _).2, (f.2 _ _ _ _).1, (f.2 _ _ _ _).1.trans (f.2 _ _ _ _).2])
invFun
F :=
⟨fun a₁ a₂ b₁ b₂ => F s(a₁, a₂) s(b₁, b₂), fun a₁ a₂ b₁ b₂ =>
by
constructor
exacts [congr_arg₂ F eq_swap rfl, congr_arg₂ F rfl eq_swap]⟩
right_inv _ := funext₂ fun a b => Sym2.inductionOn₂ a b fun _ _ _ _ => rfl
