Common.Set.Function

Additional theorems around functions defined on sets.

def Set.Function.swap {α : Sort u_1} {β : Sort u_2} [DecidableEq α] (f : α → β) (x₁ : α) (x₂ : α) (x : α) : β

Produce a new function that swaps the outputs of the two specified inputs.

Equations

• Set.Function.swap f x₁ x₂ x = if x = x₁ then f x₂ else if x = x₂ then f x₁ else f x

@[simp]

theorem Set.Function.swap_eq_eq_self {α : Sort u_1} {β : Sort u_2} [DecidableEq α] {f : α → β} {x : α} : Set.Function.swap f x x = f

Swapping the same input yields the original function.

@[simp]

theorem Set.Function.swap_swap_eq_self {α : Sort u_1} {β : Sort u_2} [DecidableEq α] {f : α → β} {x₁ : α} {x₂ : α} : Set.Function.swap (Set.Function.swap f x₁ x₂) x₁ x₂ = f

Swapping a function twice yields the original function.

theorem Set.Function.swap_MapsTo_self {α : Type u_1} {β : Type u_2} {a₁ : α} {a₂ : α} [DecidableEq α] {A : Set α} {B : Set β} {f : α → β} (ha₁ : a₁ ∈ A) (ha₂ : a₂ ∈ A) (hf : Set.MapsTo f A B) : Set.MapsTo (Set.Function.swap f a₁ a₂) A B

If f : A → B, then a swapped variant of f also maps A into B.

theorem Set.Function.self_MapsTo_swap {α : Type u_1} {β : Type u_2} {a₁ : α} {a₂ : α} [DecidableEq α] {A : Set α} {B : Set β} {f : α → β} (ha₁ : a₁ ∈ A) (ha₂ : a₂ ∈ A) (hf : Set.MapsTo (Set.Function.swap f a₁ a₂) A B) : Set.MapsTo f A B

The converse of swap_MapsTo_self.

theorem Set.Function.self_iff_swap_MapsTo {α : Type u_1} {β : Type u_2} {a₁ : α} {a₂ : α} [DecidableEq α] {A : Set α} {B : Set β} {f : α → β} (ha₁ : a₁ ∈ A) (ha₂ : a₂ ∈ A) : Set.MapsTo (Set.Function.swap f a₁ a₂) A B ↔ Set.MapsTo f A B

If f : A → B, then f maps A into B iff a swap of f maps A into B.

theorem Set.Function.swap_InjOn_self {α : Type u_1} {β : Type u_2} {a₁ : α} {a₂ : α} [DecidableEq α] {A : Set α} {f : α → β} (ha₁ : a₁ ∈ A) (ha₂ : a₂ ∈ A) (hf : Set.InjOn f A) : Set.InjOn (Set.Function.swap f a₁ a₂) A

If f : A → B is one-to-one, then a swapped variant of f is also one-to-one.

theorem Set.Function.self_InjOn_swap {α : Type u_1} {β : Type u_2} {a₁ : α} {a₂ : α} [DecidableEq α] {A : Set α} {f : α → β} (ha₁ : a₁ ∈ A) (ha₂ : a₂ ∈ A) (hf : Set.InjOn (Set.Function.swap f a₁ a₂) A) : Set.InjOn f A

The converse of swap_InjOn_self.

theorem Set.Function.self_iff_swap_InjOn {α : Type u_1} {β : Type u_2} {a₁ : α} {a₂ : α} [DecidableEq α] {A : Set α} {f : α → β} (ha₁ : a₁ ∈ A) (ha₂ : a₂ ∈ A) : Set.InjOn (Set.Function.swap f a₁ a₂) A ↔ Set.InjOn f A

If f : A → B, then f is one-to-one iff a swap of f is one-to-one.

theorem Set.Function.swap_SurjOn_self {α : Type u_1} {β : Type u_2} {a₁ : α} {a₂ : α} [DecidableEq α] {A : Set α} {B : Set β} {f : α → β} (ha₁ : a₁ ∈ A) (ha₂ : a₂ ∈ A) (hf : Set.SurjOn f A B) : Set.SurjOn (Set.Function.swap f a₁ a₂) A B

If f : A → B is onto, then a swapped variant of f is also onto.

theorem Set.Function.self_SurjOn_swap {α : Type u_1} {β : Type u_2} {a₁ : α} {a₂ : α} [DecidableEq α] {A : Set α} {B : Set β} {f : α → β} (ha₁ : a₁ ∈ A) (ha₂ : a₂ ∈ A) (hf : Set.SurjOn (Set.Function.swap f a₁ a₂) A B) : Set.SurjOn f A B

The converse of swap_SurjOn_self.

theorem Set.Function.self_iff_swap_SurjOn {α : Type u_1} {β : Type u_2} {a₁ : α} {a₂ : α} [DecidableEq α] {A : Set α} {B : Set β} {f : α → β} (ha₁ : a₁ ∈ A) (ha₂ : a₂ ∈ A) : Set.SurjOn (Set.Function.swap f a₁ a₂) A B ↔ Set.SurjOn f A B

If f : A → B, then f is onto iff a swap of f is onto.

theorem Set.Function.swap_BijOn_self {α : Type u_1} {β : Type u_2} {a₁ : α} {a₂ : α} [DecidableEq α] {A : Set α} {B : Set β} {f : α → β} (ha₁ : a₁ ∈ A) (ha₂ : a₂ ∈ A) (hf : Set.BijOn f A B) : Set.BijOn (Set.Function.swap f a₁ a₂) A B

If f : A → B is a one-to-one correspondence, then a swapped variant of f is also a one-to-one correspondence.

theorem Set.Function.self_BijOn_swap {α : Type u_1} {β : Type u_2} {a₁ : α} {a₂ : α} [DecidableEq α] {A : Set α} {B : Set β} {f : α → β} (ha₁ : a₁ ∈ A) (ha₂ : a₂ ∈ A) (hf : Set.BijOn (Set.Function.swap f a₁ a₂) A B) : Set.BijOn f A B

The converse of swap_BijOn_self.

theorem Set.Function.self_iff_swap_BijOn {α : Type u_1} {β : Type u_2} {a₁ : α} {a₂ : α} [DecidableEq α] {A : Set α} {B : Set β} {f : α → β} (ha₁ : a₁ ∈ A) (ha₂ : a₂ ∈ A) : Set.BijOn (Set.Function.swap f a₁ a₂) A B ↔ Set.BijOn f A B

If f : A → B, f is a one-to-one correspondence iff a swap of f is a one-to-one correspondence.