structure Inverse {α : Type u_1} {β : Type u_2} (f : α → β) (g : β → α) : Prop

• fg {x : β} : f (g x) = x
• gf {x : α} : g (f x) = x

structure BijectiveOn {α : Type u_1} {β : Type u_2} (pa : α → Prop) (pb : β → Prop) (f : α → β) (f' : β → α) : Prop

• h : ∃ (e : { x : α // pa x } ≃ { y : β // pb y }), (∀ {x : α} (hx : pa x), f x = ↑(e ⟨x, hx⟩)) ∧ ∀ {y : β} (hy : pb y), f' y = ↑(e.symm ⟨y, hy⟩)

structure StrictBijectiveOn {α : Type u_1} {β : Type u_2} (pa : α → Prop) (pb : β → Prop) (f : α → β) (f' : β → α) extends BijectiveOn pa pb f f' : Prop

• h : ∃ (e : { x : α // pa x } ≃ { y : β // pb y }), (∀ {x : α} (hx : pa x), f x = ↑(e ⟨x, hx⟩)) ∧ ∀ {y : β} (hy : pb y), f' y = ↑(e.symm ⟨y, hy⟩)
• cnd_of_right {x : α} : pb (f x) → pa x
• cnd_of_left {y : β} : pa (f' y) → pb y

def fn_set' {α : Type u_1} [DecidableEq α] (a b x : α) : α

Equations

• fn_set' a b x = if x = a then b else x

def fn_swap' {α : Type u_1} [DecidableEq α] (a b x : α) : α

Equations

• fn_swap' a b x = if x = a then b else if x = b then a else x

def fn_set {α : Type u_1} {β : Type u_2} [DecidableEq α] (a : α) (b : β) (f : α → β) (x : α) : β

Equations

• fn_set a b f x = if x = a then b else f x

def fn_swap {α : Type u_1} {β : Type u_2} [DecidableEq α] (a b : α) (f : α → β) (x : α) : β

Equations

• fn_swap a b f x = f (fn_swap' a b x)

def Function.fixNCnd {α : Type u_1} (f : α → α) (x : α) (k : ℕ) : Prop

Equations

• Function.fixNCnd f x k = Function.IsFixedPt f (f^[k] x)

noncomputable def Function.fixN {α : Type u_1} (f : α → α) (x : α) : ℕ

Equations

• Function.fixN f x = Classical.epsilon fun (y : ℕ) => Function.fixNCnd f x y

noncomputable def Function.fix {α : Type u_1} (f : α → α) (x : α) : α

Equations

• Function.fix f x = f^[Function.fixN f x] x

def Function.fixCnd {α : Type u_1} (f : α → α) (x : α) (k : ℕ) : Prop

Equations

• Function.fixCnd f x k = (Function.fix f x = f^[k] x ∧ f (Function.fix f x) = Function.fix f x)

theorem fn_set_eq {α : Type u_1} {β : Type u_2} [DecidableEq α] {a : α} {b : β} {f : α → β} {x : α} : fn_set a b f x = if x = a then b else f x

theorem fn_swap_eq {α : Type u_1} {β : Type u_2} [DecidableEq α] {a b : α} {f : α → β} {x : α} : fn_swap a b f x = f (if x = a then b else if x = b then a else x)

@[simp]

theorem fn_swap'_idemp {α : Type u_1} [DecidableEq α] {a b x : α} : fn_swap' a b (fn_swap' a b x) = x

@[simp]

theorem fn_swap_idemp {α : Type u_1} {β : Type u_2} [DecidableEq α] {a b : α} {f : α → β} : fn_swap a b (fn_swap a b f) = f

def fn_swap'_equiv {α : Type u_1} [DecidableEq α] (a b : α) : α ≃ α

Equations

• fn_swap'_equiv a b = { toFun := fn_swap' a b, invFun := fn_swap' a b, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem fn_swap'_equiv_to_fun {α : Type u_1} [DecidableEq α] {a b : α} : (fn_swap'_equiv a b).toFun = fn_swap' a b

@[simp]

theorem fn_swap'_equiv_inv_fun {α : Type u_1} [DecidableEq α] {a b : α} : (fn_swap'_equiv a b).invFun = fn_swap' a b

@[simp]

theorem fn_swap'_equiv_apply {α : Type u_1} [DecidableEq α] {a b x : α} : (fn_swap'_equiv a b) x = fn_swap' a b x

@[simp]

theorem fn_set'_eq_of_eq {α : Type u_1} [DecidableEq α] {a b : α} : fn_set' a b a = b

@[simp]

theorem fn_swap'_eq_of_eq_left {α : Type u_1} [DecidableEq α] {a b : α} : fn_swap' a b a = b

@[simp]

theorem fn_swap'_eq_of_eq_right {α : Type u_1} [DecidableEq α] {a b : α} : fn_swap' a b b = a

@[simp]

theorem fn_set_eq_of_eq {α : Type u_1} {β : Type u_2} [DecidableEq α] {a : α} {b : β} {f : α → β} : fn_set a b f a = b

@[simp]

theorem fn_swap_eq_of_eq_left {α : Type u_1} {β : Type u_2} [DecidableEq α] {a b : α} {f : α → β} : fn_swap a b f a = f b

@[simp]

theorem fn_swap_eq_of_eq_right {α : Type u_1} {β : Type u_2} [DecidableEq α] {a b : α} {f : α → β} : fn_swap a b f b = f a

theorem fn_set_eq_of_ne {α : Type u_1} {β : Type u_2} [DecidableEq α] {a : α} {b : β} {f : α → β} {x : α} (hx : x ≠ a) : fn_set a b f x = f x

theorem fn_set_fn_set_eq_fn_swap {α : Type u_1} {β : Type u_2} [DecidableEq α] {a b : α} {f : α → β} : fn_set a (f b) (fn_set b (f a) f) = fn_swap a b f

theorem fn_set_same_value {α : Type u_1} {β : Type u_2} [DecidableEq α] {f : α → β} {a : α} : fn_set a (f a) f = f

theorem fn_set_twice_same {α : Type u_1} {β : Type u_2} [DecidableEq α] {f : α → β} {a : α} {b₁ b₂ : β} : fn_set a b₂ (fn_set a b₁ f) = fn_set a b₂ f

theorem fn_set_comm {α : Type u_1} {β : Type u_2} [DecidableEq α] {f : α → β} {a₁ a₂ : α} {b₁ b₂ : β} (h : a₁ ≠ a₂) : fn_set a₁ b₁ (fn_set a₂ b₂ f) = fn_set a₂ b₂ (fn_set a₁ b₁ f)

theorem fn_set_ext {α : Type u_1} {β : Type u_2} [DecidableEq α] {f g : α → β} {a : α} {b : β} : (∀ (x : α), fn_set a b f x = fn_set a b g x) ↔ ∀ (x : α), x ≠ a → f x = g x

@[simp]

theorem inverse_id {α : Type u_1} : Inverse id id

@[simp]

theorem leftInverse_id {α : Type u_1} : Function.LeftInverse id id

@[simp]

theorem rightInverse_id {α : Type u_1} : Function.RightInverse id id

@[simp]

theorem bijectiveOn_id {α : Type u_1} {pa : α → Prop} : BijectiveOn pa pa id id

theorem BijectiveOn.cnd_right {α : Type u_1} {β : Type u_2} {pa : α → Prop} {pb : β → Prop} {f : α → β} {f' : β → α} {H : BijectiveOn pa pb f f'} {x : α} (h : pa x) : pb (f x)

theorem BijectiveOn.cnd_left {α : Type u_1} {β : Type u_2} {pa : α → Prop} {pb : β → Prop} {f : α → β} {f' : β → α} {H : BijectiveOn pa pb f f'} {y : β} (h : pb y) : pa (f' y)

theorem BijectiveOn.cancel_left {α : Type u_1} {β : Type u_2} {pa : α → Prop} {pb : β → Prop} {f : α → β} {f' : β → α} {H : BijectiveOn pa pb f f'} {x : α} (h : pa x) : f' (f x) = x

theorem BijectiveOn.cancel_right {α : Type u_1} {β : Type u_2} {pa : α → Prop} {pb : β → Prop} {f : α → β} {f' : β → α} {H : BijectiveOn pa pb f f'} {y : β} (h : pb y) : f (f' y) = y

theorem BijectiveOn.symm {α : Type u_1} {β : Type u_2} {pa : α → Prop} {pb : β → Prop} {f : α → β} {f' : β → α} {H : BijectiveOn pa pb f f'} : BijectiveOn pb pa f' f

@[simp]

theorem strictBijectiveOn_id {α : Type u_1} {pa : α → Prop} : StrictBijectiveOn pa pa id id

theorem StrictBijectiveOn.symm {α : Type u_1} {β : Type u_2} {pa : α → Prop} {pb : β → Prop} {f : α → β} {f' : β → α} {H : StrictBijectiveOn pa pb f f'} : StrictBijectiveOn pb pa f' f

def Equiv.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e₁ : β ≃ γ) (e₂ : α ≃ β) : α ≃ γ

Equations

• e₁.comp e₂ = { toFun := ⇑e₁ ∘ ⇑e₂, invFun := ⇑e₂.symm ∘ ⇑e₁.symm, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Equiv.coe_toFun_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {e₁ : β ≃ γ} {e₂ : α ≃ β} : ⇑(e₁.comp e₂) = ⇑e₁ ∘ ⇑e₂

@[simp]

theorem Equiv.symm_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {e₁ : β ≃ γ} {e₂ : α ≃ β} : (e₁.comp e₂).symm = e₂.symm.comp e₁.symm

theorem Inverse.symm {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} {H : Inverse f g} : Inverse g f

theorem Equiv.forall_iff {α : Type u_1} {β : Type u_2} {e : α ≃ β} {p : α → Prop} : (∀ (x : α), p x) ↔ ∀ (y : β), p (e.symm y)

theorem Equiv.forall_iff' {α : Type u_1} {β : Type u_2} {e : α ≃ β} {p : β → Prop} : (∀ (x : β), p x) ↔ ∀ (y : α), p (e y)

@[simp]

theorem Equiv.mk_symm {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} {h₁ : Function.LeftInverse g f} {h₂ : Function.RightInverse g f} : { toFun := f, invFun := g, left_inv := h₁, right_inv := h₂ }.symm = { toFun := g, invFun := f, left_inv := h₂, right_inv := h₁ }

def FinFn {n : ℕ} (α : Fin n → Type u) (β : Type v) : Type ((max u v) + 1)

Equations

• FinFn α_2 β = ULift.{(max ?u.2 ?u.1) + 1, ?u.1} β
• FinFn α_2 β = (α_2 0 → FinFn (fun (k : Fin n_2) => α_2 ⟨↑k + 1, ⋯⟩) β)

def mkFinFn {n : ℕ} {α : Fin n → Type u} {β : Type v} (f : ((n : Fin n) → α n) → β) : FinFn α β

Equations

• mkFinFn f = Nat.recAux (motive := fun {n : ℕ} => {α : Fin n → Type ?u.2} → (((n : Fin n) → α n) → β) → FinFn α β) (fun {α : Fin 0 → Type ?u.2} (f : ((n : Fin 0) → α n) → β) => { down := f fun (a : Fin 0) => nomatch a }) (fun (n : ℕ) (a : {α : Fin n → Type ?u.2} → (((n : Fin n) → α n) → β) → FinFn α β) {α : Fin (n + 1) → Type ?u.2} (f : ((n : Fin (n + 1)) → α n) → β) (x : α 0) => a fun (ps : (n_1 : Fin n) → Fin.casesOn n_1 fun (k : ℕ) (hk : k < n) => α ⟨k + 1, ⋯⟩) => f fun (n_1 : Fin (n + 1)) => Fin.casesOn n_1 fun (k : ℕ) (hk : k < n + 1) => Nat.casesAuxOn (motive := fun (a : ℕ) => k = a → α ⟨k, hk⟩) k (fun (h : k = 0) => Eq.ndrec (motive := fun (k : ℕ) => (hk : k < n + 1) → α ⟨k, hk⟩) (fun (hk : 0 < n + 1) => x) ⋯ hk) (fun (n_2 : ℕ) (h : k = n_2 + 1) => Eq.ndrec (motive := fun (k : ℕ) => (hk : k < n + 1) → α ⟨k, hk⟩) (fun (hk : n_2 + 1 < n + 1) => ⋯.mpr (ps ⟨n_2, ⋯⟩)) ⋯ hk) ⋯) n f

def callFinFn {n : ℕ} {α : Fin n → Type u} {β : Type v} (f : FinFn α β) (ps : (n : Fin n) → α n) : β

Equations

• callFinFn f_2 ps_2 = f_2.down
• callFinFn f_2 ps_2 = callFinFn (f_2 (ps_2 0)) fun (k : Fin n_2) => ps_2 ⟨↑k + 1, ⋯⟩

theorem Function.iterate_add' {α : Type u_1} {f : α → α} {n m : ℕ} : f^[n + m] = f^[m] ∘ f^[n]

theorem Function.fixCnd_spec {α : Type u_1} {f : α → α} {x : α} (k : ℕ) (h : IsFixedPt f (f^[k] x)) : fixNCnd f x (fixN f x)

theorem Function.fix_spec {α : Type u_1} {f : α → α} {x : α} (k : ℕ) (h : IsFixedPt f (f^[k] x)) : fixCnd f x k

theorem Function.fix_spec' {α : Type u_1} {f : α → α} {x : α} (k : ℕ) (h : IsFixedPt f (f^[k] x)) : fixCnd f x (fixN f x)

theorem Function.fixCnd_fixN_of_fixCnd {α : Type u_1} {f : α → α} {x : α} {k : ℕ} (h : fixCnd f x k) : fixCnd f x (fixN f x)

theorem Function.fixCnd_apply {α : Type u_1} {f : α → α} {x : α} {k : ℕ} (h : fixCnd f x k) : fixCnd f (f x) k

theorem Function.fix_apply {α : Type u_1} {f : α → α} {x : α} {k : ℕ} (h : fixCnd f x k) : fix f (f x) = fix f x