chore(Logic/Function/OfArity): rename Arity to Function.OfArity (#…

…7772)

Also puts it in a new file.

Mathlib.lean

@@ -2395,6 +2395,7 @@ import Mathlib.Logic.Equiv.TransferInstance
 import Mathlib.Logic.Function.Basic
 import Mathlib.Logic.Function.Conjugate
 import Mathlib.Logic.Function.Iterate
+import Mathlib.Logic.Function.OfArity
 import Mathlib.Logic.Hydra
 import Mathlib.Logic.IsEmpty
 import Mathlib.Logic.Lemmas

Mathlib/Logic/Function/OfArity.lean

@@ -0,0 +1,69 @@
+/-
+Copyright (c) 2017 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+
+import Mathlib.Init.Data.Nat.Notation
+import Mathlib.Mathport.Rename
+
+/-! # Function types of a given arity
+
+This provides `FunctionOfArity`, such that `OfArity α 2 = α → α → α`.
+Note that it is often preferrable to use `(Fin n → α) → α` in place of `OfArity n α`.
+
+## Main definitions
+
+* `Function.OfArity α n`: `n`-ary function `α → α → ... → α`. Defined inductively.
+* `Function.OfArity.const a n`: `n`-ary constant function equal to `a`.
+-/
+
+universe u
+
+namespace Function
+
+/-- The type of `n`-ary functions `α → α → ... → α`. -/
+def OfArity (α : Type u) : ℕ → Type u
+  | 0 => α
+  | n + 1 => α → OfArity α n
+#align arity Function.OfArity
+
+@[simp]
+theorem ofArity_zero (α : Type u) : OfArity α 0 = α :=
+  rfl
+#align arity_zero Function.ofArity_zero
+
+@[simp]
+theorem ofArity_succ (α : Type u) (n : ℕ) : OfArity α n.succ = (α → OfArity α n) :=
+  rfl
+#align arity_succ Function.ofArity_succ
+
+namespace OfArity
+
+/-- Constant `n`-ary function with value `a`. -/
+def const {α : Type u} (a : α) : ∀ n, OfArity α n
+  | 0 => a
+  | n + 1 => fun _ => const a n
+#align arity.const Function.OfArity.const
+
+@[simp]
+theorem const_zero {α : Type u} (a : α) : const a 0 = a :=
+  rfl
+#align arity.const_zero Function.OfArity.const_zero
+
+@[simp]
+theorem const_succ {α : Type u} (a : α) (n : ℕ) : const a n.succ = fun _ => const a n :=
+  rfl
+#align arity.const_succ Function.OfArity.const_succ
+
+theorem const_succ_apply {α : Type u} (a : α) (n : ℕ) (x : α) : const a n.succ x = const a n :=
+  rfl
+#align arity.const_succ_apply Function.OfArity.const_succ_apply
+
+instance OfArity.inhabited {α n} [Inhabited α] : Inhabited (OfArity α n) :=
+  ⟨const default _⟩
+#align arity.arity.inhabited Function.OfArity.OfArity.inhabited
+
+end OfArity
+
+end Function

Mathlib/SetTheory/ZFC/Basic.lean

@@ -5,6 +5,7 @@ Authors: Mario Carneiro
 -/
 import Mathlib.Data.Set.Lattice
 import Mathlib.Logic.Small.Basic
+import Mathlib.Logic.Function.OfArity
 import Mathlib.Order.WellFounded
 
 #align_import set_theory.zfc.basic from "leanprover-community/mathlib"@"f0b3759a8ef0bd8239ecdaa5e1089add5feebe1a"
@@ -30,8 +31,6 @@ Then the rest is usual set theory.
 
 ## Other definitions
 
-* `Arity α n`: `n`-ary function `α → α → ... → α`. Defined inductively.
-* `Arity.const a n`: `n`-ary constant function equal to `a`.
 * `PSet.Type`: Underlying type of a pre-set.
 * `PSet.Func`: Underlying family of pre-sets of a pre-set.
 * `PSet.Equiv`: Extensional equivalence of pre-sets. Defined inductively.
@@ -65,49 +64,7 @@ set_option linter.uppercaseLean3 false
 
 universe u v
 
-/-- The type of `n`-ary functions `α → α → ... → α`. -/
-def Arity (α : Type u) : ℕ → Type u
-  | 0 => α
-  | n + 1 => α → Arity α n
-#align arity Arity
-
-@[simp]
-theorem arity_zero (α : Type u) : Arity α 0 = α :=
-  rfl
-#align arity_zero arity_zero
-
-@[simp]
-theorem arity_succ (α : Type u) (n : ℕ) : Arity α n.succ = (α → Arity α n) :=
-  rfl
-#align arity_succ arity_succ
-
-namespace Arity
-
-/-- Constant `n`-ary function with value `a`. -/
-def const {α : Type u} (a : α) : ∀ n, Arity α n
-  | 0 => a
-  | n + 1 => fun _ => const a n
-#align arity.const Arity.const
-
-@[simp]
-theorem const_zero {α : Type u} (a : α) : const a 0 = a :=
-  rfl
-#align arity.const_zero Arity.const_zero
-
-@[simp]
-theorem const_succ {α : Type u} (a : α) (n : ℕ) : const a n.succ = fun _ => const a n :=
-  rfl
-#align arity.const_succ Arity.const_succ
-
-theorem const_succ_apply {α : Type u} (a : α) (n : ℕ) (x : α) : const a n.succ x = const a n :=
-  rfl
-#align arity.const_succ_apply Arity.const_succ_apply
-
-instance Arity.inhabited {α n} [Inhabited α] : Inhabited (Arity α n) :=
-  ⟨const default _⟩
-#align arity.arity.inhabited Arity.Arity.inhabited
-
-end Arity
+open Function (OfArity)
 
 /-- The type of pre-sets in universe `u`. A pre-set
   is a family of pre-sets indexed by a type in `Type u`.
@@ -526,24 +483,24 @@ theorem lift_mem_embed : ∀ x : PSet.{u}, PSet.Lift.{u, max (u + 1) v} x ∈ em
 
 /-- Function equivalence is defined so that `f ~ g` iff `∀ x y, x ~ y → f x ~ g y`. This extends to
 equivalence of `n`-ary functions. -/
-def Arity.Equiv : ∀ {n}, Arity PSet.{u} n → Arity PSet.{u} n → Prop
+def Arity.Equiv : ∀ {n}, OfArity PSet.{u} n → OfArity PSet.{u} n → Prop
   | 0, a, b => PSet.Equiv a b
   | _ + 1, a, b => ∀ x y : PSet, PSet.Equiv x y → Arity.Equiv (a x) (b y)
 #align pSet.arity.equiv PSet.Arity.Equiv
 
-theorem Arity.equiv_const {a : PSet.{u}} : ∀ n, Arity.Equiv (Arity.const a n) (Arity.const a n)
+theorem Arity.equiv_const {a : PSet.{u}} : ∀ n, Arity.Equiv (OfArity.const a n) (OfArity.const a n)
   | 0 => Equiv.rfl
   | _ + 1 => fun _ _ _ => Arity.equiv_const _
 #align pSet.arity.equiv_const PSet.Arity.equiv_const
 
 /-- `resp n` is the collection of n-ary functions on `PSet` that respect
   equivalence, i.e. when the inputs are equivalent the output is as well. -/
 def Resp (n) :=
-  { x : Arity PSet.{u} n // Arity.Equiv x x }
+  { x : OfArity PSet.{u} n // Arity.Equiv x x }
 #align pSet.resp PSet.Resp
 
 instance Resp.inhabited {n} : Inhabited (Resp n) :=
-  ⟨⟨Arity.const default _, Arity.equiv_const _⟩⟩
+  ⟨⟨OfArity.const default _, Arity.equiv_const _⟩⟩
 #align pSet.resp.inhabited PSet.Resp.inhabited
 
 /-- The `n`-ary image of a `(n + 1)`-ary function respecting equivalence as a function respecting
@@ -598,10 +555,10 @@ namespace Resp
 
 /-- Helper function for `PSet.eval`. -/
 def evalAux :
-    ∀ {n}, { f : Resp n → Arity ZFSet.{u} n // ∀ a b : Resp n, Resp.Equiv a b → f a = f b }
+    ∀ {n}, { f : Resp n → OfArity ZFSet.{u} n // ∀ a b : Resp n, Resp.Equiv a b → f a = f b }
   | 0 => ⟨fun a => ⟦a.1⟧, fun _ _ h => Quotient.sound h⟩
   | n + 1 =>
-    let F : Resp (n + 1) → Arity ZFSet (n + 1) := fun a =>
+    let F : Resp (n + 1) → OfArity ZFSet (n + 1) := fun a =>
       @Quotient.lift _ _ PSet.setoid (fun x => evalAux.1 (a.f x)) fun _ _ h =>
         evalAux.2 _ _ (a.2 _ _ h)
     ⟨F, fun b c h =>
@@ -611,11 +568,11 @@ def evalAux :
 #align pSet.resp.eval_aux PSet.Resp.evalAux
 
 /-- An equivalence-respecting function yields an n-ary ZFC set function. -/
-def eval (n) : Resp n → Arity ZFSet.{u} n :=
+def eval (n) : Resp n → OfArity ZFSet.{u} n :=
   evalAux.1
 #align pSet.resp.eval PSet.Resp.eval
 
-theorem eval_val {n f x} : (@eval (n + 1) f : ZFSet → Arity ZFSet n) ⟦x⟧ = eval n (Resp.f f x) :=
+theorem eval_val {n f x} : (@eval (n + 1) f : ZFSet → OfArity ZFSet n) ⟦x⟧ = eval n (Resp.f f x) :=
   rfl
 #align pSet.resp.eval_val PSet.Resp.eval_val
 
@@ -624,24 +581,24 @@ end Resp
 /-- A set function is "definable" if it is the image of some n-ary pre-set
   function. This isn't exactly definability, but is useful as a sufficient
   condition for functions that have a computable image. -/
-class inductive Definable (n) : Arity ZFSet.{u} n → Type (u + 1)
+class inductive Definable (n) : OfArity ZFSet.{u} n → Type (u + 1)
   | mk (f) : Definable n (Resp.eval n f)
 #align pSet.definable PSet.Definable
 
 attribute [instance] Definable.mk
 
 /-- The evaluation of a function respecting equivalence is definable, by that same function. -/
-def Definable.EqMk {n} (f) : ∀ {s : Arity ZFSet.{u} n} (_ : Resp.eval _ f = s), Definable n s
+def Definable.EqMk {n} (f) : ∀ {s : OfArity ZFSet.{u} n} (_ : Resp.eval _ f = s), Definable n s
   | _, rfl => ⟨f⟩
 #align pSet.definable.eq_mk PSet.Definable.EqMk
 
 /-- Turns a definable function into a function that respects equivalence. -/
-def Definable.Resp {n} : ∀ (s : Arity ZFSet.{u} n) [Definable n s], Resp n
+def Definable.Resp {n} : ∀ (s : OfArity ZFSet.{u} n) [Definable n s], Resp n
   | _, ⟨f⟩ => f
 #align pSet.definable.resp PSet.Definable.Resp
 
 theorem Definable.eq {n} :
-    ∀ (s : Arity ZFSet.{u} n) [H : Definable n s], (@Definable.Resp n s H).eval _ = s
+    ∀ (s : OfArity ZFSet.{u} n) [H : Definable n s], (@Definable.Resp n s H).eval _ = s
   | _, ⟨_⟩ => rfl
 #align pSet.definable.eq PSet.Definable.eq
 
@@ -652,11 +609,11 @@ namespace Classical
 open PSet
 
 /-- All functions are classically definable. -/
-noncomputable def allDefinable : ∀ {n} (F : Arity ZFSet n), Definable n F
+noncomputable def allDefinable : ∀ {n} (F : OfArity ZFSet n), Definable n F
   | 0, F =>
     let p := @Quotient.exists_rep PSet _ F
     @Definable.EqMk 0 ⟨choose p, Equiv.rfl⟩ _ (choose_spec p)
-  | n + 1, (F : Arity ZFSet (n + 1)) => by
+  | n + 1, (F : OfArity ZFSet (n + 1)) => by
     have I := fun x => allDefinable (F x)
     refine' @Definable.EqMk (n + 1) ⟨fun x : PSet => (@Definable.Resp _ _ (I ⟦x⟧)).1, _⟩ _ _
     · dsimp [Arity.Equiv]
@@ -703,7 +660,7 @@ theorem exact {x y : PSet} : mk x = mk y → PSet.Equiv x y :=
 
 @[simp]
 theorem eval_mk {n f x} :
-    (@Resp.eval (n + 1) f : ZFSet → Arity ZFSet n) (mk x) = Resp.eval n (Resp.f f x) :=
+    (@Resp.eval (n + 1) f : ZFSet → OfArity ZFSet n) (mk x) = Resp.eval n (Resp.f f x) :=
   rfl
 #align Set.eval_mk ZFSet.eval_mk