Documentation

Mathlib.Data.PEquiv

Partial Equivalences #

In this file, we define partial equivalences PEquiv, which are a bijection between a subset of α and a subset of β. Notationally, a PEquiv is denoted by "≃.≃." (note that the full stop is part of the notation). The way we store these internally is with two functions f : α → Option β→ Option β and the reverse function g : β → Option α→ Option α, with the condition that if f a is some b, then g b is some a.

Main results #

PEquiv.ofSet: creates a PEquiv from a set s, which sends an element to itself if it is in s.
PEquiv.single: given two elements a : α and b : β, create a PEquiv that sends them to each other, and ignores all other elements.
PEquiv.injective_of_forall_ne_isSome/injective_of_forall_isSome: If the domain of a PEquiv is all of α (except possibly one point), its toFun is injective.

Canonical order #

PEquiv is canonically ordered by inclusion; that is, if a function f defined on a subset s is equal to g on that subset, but g is also defined on a larger set, then f ≤ g≤ g. We also have a definition of ⊥⊥, which is the empty PEquiv (sends all to none), which in the end gives us a SemilatticeInf with an OrderBot instance.

Tags #

pequiv, partial equivalence

structure PEquiv (α : Type u) (β : Type v) :

Type (maxuv)

The underlying partial function of a PEquiv
toFun : α → Option β
The partial inverse of toFun
invFun : β → Option α
invFun is the partial inverse of toFun
inv : ∀ (a : α) (b : β), a ∈ invFun b ↔ b ∈ toFun a

A PEquiv is a partial equivalence, a representation of a bijection between a subset of α and a subset of β. See also LocalEquiv for a version that requires toFun and invFun to be globally defined functions and has source and target sets as extra fields.

Instances For

def «term_≃._» :

Lean.TrailingParserDescr

A PEquiv is a partial equivalence, a representation of a bijection between a subset of α and a subset of β. See also LocalEquiv for a version that requires toFun and invFun to be globally defined functions and has source and target sets as extra fields.

Equations

«term_≃._» = Lean.ParserDescr.trailingNode `term_≃._ 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃. ") (Lean.ParserDescr.cat `term 25))

instance PEquiv.instFunLikePEquivOption {α : Type u} {β : Type v} :

FunLike (α ≃. β) α fun x => Option β

Equations

PEquiv.instFunLikePEquivOption = { coe := PEquiv.toFun, coe_injective' := (_ : ∀ ⦃a₁ a₂ : α ≃. β⦄, a₁.toFun = a₂.toFun → a₁ = a₂) }

@[simp]

theorem PEquiv.coe_mk {α : Type u} {β : Type v} (f₁ : α → Option β) (f₂ : β → Option α) (h : ∀ (a : α) (b : β), a ∈ f₂ b ↔ b ∈ f₁ a) :

↑{ toFun := f₁, invFun := f₂, inv := h } = f₁

theorem PEquiv.coe_mk_apply {α : Type u} {β : Type v} (f₁ : α → Option β) (f₂ : β → Option α) (h : ∀ (a : α) (b : β), a ∈ f₂ b ↔ b ∈ f₁ a) (x : α) :

↑{ toFun := f₁, invFun := f₂, inv := h } x = f₁ x

theorem PEquiv.ext {α : Type u} {β : Type v} {f : α ≃. β} {g : α ≃. β} (h : ∀ (x : α), ↑f x = ↑g x) :

f = g

theorem PEquiv.ext_iff {α : Type u} {β : Type v} {f : α ≃. β} {g : α ≃. β} :

f = g ↔ ∀ (x : α), ↑f x = ↑g x

def PEquiv.refl (α : Type u_1) :

α ≃. α

The identity map as a partial equivalence.

Equations

PEquiv.refl α = { toFun := some, invFun := some, inv := (_ : ∀ (x x_1 : α), some x_1 = some x ↔ some x = some x_1) }

def PEquiv.symm {α : Type u} {β : Type v} (f : α ≃. β) :

β ≃. α

The inverse partial equivalence.

Equations

PEquiv.symm f = { toFun := f.invFun, invFun := f.toFun, inv := (_ : ∀ (x : β) (x_1 : α), x ∈ PEquiv.toFun f x_1 ↔ x_1 ∈ PEquiv.invFun f x) }

theorem PEquiv.mem_iff_mem {α : Type u} {β : Type v} (f : α ≃. β) {a : α} {b : β} :

a ∈ ↑(PEquiv.symm f) b ↔ b ∈ ↑f a

theorem PEquiv.eq_some_iff {α : Type u} {β : Type v} (f : α ≃. β) {a : α} {b : β} :

↑(PEquiv.symm f) b = some a ↔ ↑f a = some b

def PEquiv.trans {α : Type u} {β : Type v} {γ : Type w} (f : α ≃. β) (g : β ≃. γ) :

α ≃. γ

Composition of partial equivalences f : α ≃. β≃. β and g : β ≃. γ≃. γ.

Equations

One or more equations did not get rendered due to their size.

@[simp]

theorem PEquiv.refl_apply {α : Type u} (a : α) :

↑(PEquiv.refl α) a = some a

@[simp]

theorem PEquiv.symm_refl {α : Type u} :

PEquiv.symm (PEquiv.refl α) = PEquiv.refl α

@[simp]

theorem PEquiv.symm_symm {α : Type u} {β : Type v} (f : α ≃. β) :

PEquiv.symm (PEquiv.symm f) = f

theorem PEquiv.symm_injective {α : Type u} {β : Type v} :

Function.Injective PEquiv.symm

theorem PEquiv.trans_assoc {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} (f : α ≃. β) (g : β ≃. γ) (h : γ ≃. δ) :

PEquiv.trans (PEquiv.trans f g) h = PEquiv.trans f (PEquiv.trans g h)

theorem PEquiv.mem_trans {α : Type u} {β : Type v} {γ : Type w} (f : α ≃. β) (g : β ≃. γ) (a : α) (c : γ) :

c ∈ ↑(PEquiv.trans f g) a ↔ ∃ b, b ∈ ↑f a ∧ c ∈ ↑g b

theorem PEquiv.trans_eq_some {α : Type u} {β : Type v} {γ : Type w} (f : α ≃. β) (g : β ≃. γ) (a : α) (c : γ) :

↑(PEquiv.trans f g) a = some c ↔ ∃ b, ↑f a = some b ∧ ↑g b = some c

theorem PEquiv.trans_eq_none {α : Type u} {β : Type v} {γ : Type w} (f : α ≃. β) (g : β ≃. γ) (a : α) :

↑(PEquiv.trans f g) a = none ↔ ∀ (b : β) (c : γ), ¬b ∈ ↑f a ∨ ¬c ∈ ↑g b

@[simp]

theorem PEquiv.refl_trans {α : Type u} {β : Type v} (f : α ≃. β) :

PEquiv.trans (PEquiv.refl α) f = f

@[simp]

theorem PEquiv.trans_refl {α : Type u} {β : Type v} (f : α ≃. β) :

PEquiv.trans f (PEquiv.refl β) = f

theorem PEquiv.inj {α : Type u} {β : Type v} (f : α ≃. β) {a₁ : α} {a₂ : α} {b : β} (h₁ : b ∈ ↑f a₁) (h₂ : b ∈ ↑f a₂) :

a₁ = a₂

theorem PEquiv.injective_of_forall_ne_isSome {α : Type u} {β : Type v} (f : α ≃. β) (a₂ : α) (h : ∀ (a₁ : α), a₁ ≠ a₂ → Option.isSome (↑f a₁) = true) :

Function.Injective ↑f

If the domain of a PEquiv is α except a point, its forward direction is injective.

theorem PEquiv.injective_of_forall_isSome {α : Type u} {β : Type v} {f : α ≃. β} (h : ∀ (a : α), Option.isSome (↑f a) = true) :

Function.Injective ↑f

If the domain of a PEquiv is all of α, its forward direction is injective.

def PEquiv.ofSet {α : Type u} (s : Set α) [inst : DecidablePred fun x => x ∈ s] :

α ≃. α

Creates a PEquiv that is the identity on s, and none outside of it.

Equations

One or more equations did not get rendered due to their size.

theorem PEquiv.mem_ofSet_self_iff {α : Type u} {s : Set α} [inst : DecidablePred fun x => x ∈ s] {a : α} :

a ∈ ↑(PEquiv.ofSet s) a ↔ a ∈ s

theorem PEquiv.mem_ofSet_iff {α : Type u} {s : Set α} [inst : DecidablePred fun x => x ∈ s] {a : α} {b : α} :

a ∈ ↑(PEquiv.ofSet s) b ↔ a = b ∧ a ∈ s

@[simp]

theorem PEquiv.ofSet_eq_some_iff {α : Type u} {s : Set α} :

∀ {x : DecidablePred fun x => x ∈ s} {a b : α}, ↑(PEquiv.ofSet s) b = some a ↔ a = b ∧ a ∈ s

theorem PEquiv.ofSet_eq_some_self_iff {α : Type u} {s : Set α} :

∀ {x : DecidablePred fun x => x ∈ s} {a : α}, ↑(PEquiv.ofSet s) a = some a ↔ a ∈ s

@[simp]

theorem PEquiv.ofSet_symm {α : Type u} (s : Set α) [inst : DecidablePred fun x => x ∈ s] :

PEquiv.symm (PEquiv.ofSet s) = PEquiv.ofSet s

@[simp]

theorem PEquiv.ofSet_univ {α : Type u} :

PEquiv.ofSet Set.univ = PEquiv.refl α

@[simp]

theorem PEquiv.ofSet_eq_refl {α : Type u} {s : Set α} [inst : DecidablePred fun x => x ∈ s] :

PEquiv.ofSet s = PEquiv.refl α ↔ s = Set.univ

theorem PEquiv.symm_trans_rev {α : Type u} {β : Type v} {γ : Type w} (f : α ≃. β) (g : β ≃. γ) :

PEquiv.symm (PEquiv.trans f g) = PEquiv.trans (PEquiv.symm g) (PEquiv.symm f)

theorem PEquiv.self_trans_symm {α : Type u} {β : Type v} (f : α ≃. β) :

PEquiv.trans f (PEquiv.symm f) = PEquiv.ofSet { a | Option.isSome (↑f a) = true }

theorem PEquiv.symm_trans_self {α : Type u} {β : Type v} (f : α ≃. β) :

PEquiv.trans (PEquiv.symm f) f = PEquiv.ofSet { b | Option.isSome (↑(PEquiv.symm f) b) = true }

theorem PEquiv.trans_symm_eq_iff_forall_isSome {α : Type u} {β : Type v} {f : α ≃. β} :

PEquiv.trans f (PEquiv.symm f) = PEquiv.refl α ↔ ∀ (a : α), Option.isSome (↑f a) = true

instance PEquiv.instBotPEquiv {α : Type u} {β : Type v} :

Bot (α ≃. β)

Equations

PEquiv.instBotPEquiv = { bot := { toFun := fun x => none, invFun := fun x => none, inv := (_ : ∀ (a : α) (a_1 : β), a ∈ none ↔ a_1 ∈ none) } }

instance PEquiv.instInhabitedPEquiv {α : Type u} {β : Type v} :

Inhabited (α ≃. β)

Equations

PEquiv.instInhabitedPEquiv = { default := ⊥ }

@[simp]

theorem PEquiv.bot_apply {α : Type u} {β : Type v} (a : α) :

↑⊥ a = none

@[simp]

theorem PEquiv.symm_bot {α : Type u} {β : Type v} :

PEquiv.symm ⊥ = ⊥

@[simp]

theorem PEquiv.trans_bot {α : Type u} {β : Type v} {γ : Type w} (f : α ≃. β) :

PEquiv.trans f ⊥ = ⊥

@[simp]

theorem PEquiv.bot_trans {α : Type u} {β : Type v} {γ : Type w} (f : β ≃. γ) :

PEquiv.trans ⊥ f = ⊥

theorem PEquiv.isSome_symm_get {α : Type u} {β : Type v} (f : α ≃. β) {a : α} (h : Option.isSome (↑f a) = true) :

Option.isSome (↑(PEquiv.symm f) (Option.get (↑f a) h)) = true

def PEquiv.single {α : Type u} {β : Type v} [inst : DecidableEq α] [inst : DecidableEq β] (a : α) (b : β) :

α ≃. β

Create a PEquiv which sends a to b and b to a, but is otherwise none.

Equations

One or more equations did not get rendered due to their size.

theorem PEquiv.mem_single {α : Type u} {β : Type v} [inst : DecidableEq α] [inst : DecidableEq β] (a : α) (b : β) :

b ∈ ↑(PEquiv.single a b) a

theorem PEquiv.mem_single_iff {α : Type u} {β : Type v} [inst : DecidableEq α] [inst : DecidableEq β] (a₁ : α) (a₂ : α) (b₁ : β) (b₂ : β) :

b₁ ∈ ↑(PEquiv.single a₂ b₂) a₁ ↔ a₁ = a₂ ∧ b₁ = b₂

@[simp]

theorem PEquiv.symm_single {α : Type u} {β : Type v} [inst : DecidableEq α] [inst : DecidableEq β] (a : α) (b : β) :

PEquiv.symm (PEquiv.single a b) = PEquiv.single b a

@[simp]

theorem PEquiv.single_apply {α : Type u} {β : Type v} [inst : DecidableEq α] [inst : DecidableEq β] (a : α) (b : β) :

↑(PEquiv.single a b) a = some b

theorem PEquiv.single_apply_of_ne {α : Type u} {β : Type v} [inst : DecidableEq α] [inst : DecidableEq β] {a₁ : α} {a₂ : α} (h : a₁ ≠ a₂) (b : β) :

↑(PEquiv.single a₁ b) a₂ = none

theorem PEquiv.single_trans_of_mem {α : Type u} {β : Type v} {γ : Type w} [inst : DecidableEq α] [inst : DecidableEq β] [inst : DecidableEq γ] (a : α) {b : β} {c : γ} {f : β ≃. γ} (h : c ∈ ↑f b) :

PEquiv.trans (PEquiv.single a b) f = PEquiv.single a c

theorem PEquiv.trans_single_of_mem {α : Type u} {β : Type v} {γ : Type w} [inst : DecidableEq α] [inst : DecidableEq β] [inst : DecidableEq γ] {a : α} {b : β} (c : γ) {f : α ≃. β} (h : b ∈ ↑f a) :

PEquiv.trans f (PEquiv.single b c) = PEquiv.single a c

@[simp]

theorem PEquiv.single_trans_single {α : Type u} {β : Type v} {γ : Type w} [inst : DecidableEq α] [inst : DecidableEq β] [inst : DecidableEq γ] (a : α) (b : β) (c : γ) :

PEquiv.trans (PEquiv.single a b) (PEquiv.single b c) = PEquiv.single a c

@[simp]

theorem PEquiv.single_subsingleton_eq_refl {α : Type u} [inst : DecidableEq α] [inst : Subsingleton α] (a : α) (b : α) :

PEquiv.single a b = PEquiv.refl α

theorem PEquiv.trans_single_of_eq_none {β : Type v} {γ : Type w} {δ : Type x} [inst : DecidableEq β] [inst : DecidableEq γ] {b : β} (c : γ) {f : δ ≃. β} (h : ↑(PEquiv.symm f) b = none) :

PEquiv.trans f (PEquiv.single b c) = ⊥

theorem PEquiv.single_trans_of_eq_none {α : Type u} {β : Type v} {δ : Type x} [inst : DecidableEq α] [inst : DecidableEq β] (a : α) {b : β} {f : β ≃. δ} (h : ↑f b = none) :

PEquiv.trans (PEquiv.single a b) f = ⊥

theorem PEquiv.single_trans_single_of_ne {α : Type u} {β : Type v} {γ : Type w} [inst : DecidableEq α] [inst : DecidableEq β] [inst : DecidableEq γ] {b₁ : β} {b₂ : β} (h : b₁ ≠ b₂) (a : α) (c : γ) :

PEquiv.trans (PEquiv.single a b₁) (PEquiv.single b₂ c) = ⊥

instance PEquiv.instPartialOrderPEquiv {α : Type u} {β : Type v} :

PartialOrder (α ≃. β)

Equations

PEquiv.instPartialOrderPEquiv = PartialOrder.mk (_ : ∀ (f g : α ≃. β), f ≤ g → g ≤ f → f = g)

theorem PEquiv.le_def {α : Type u} {β : Type v} {f : α ≃. β} {g : α ≃. β} :

f ≤ g ↔ ∀ (a : α) (b : β), b ∈ ↑f a → b ∈ ↑g a

instance PEquiv.instOrderBotPEquivToLEToPreorderInstPartialOrderPEquiv {α : Type u} {β : Type v} :

OrderBot (α ≃. β)

Equations

PEquiv.instOrderBotPEquivToLEToPreorderInstPartialOrderPEquiv = let src := PEquiv.instBotPEquiv; OrderBot.mk (_ : ∀ (x : α ≃. β) (x_1 : α) (x_2 : β), x_2 ∈ ↑⊥ x_1 → x_2 ∈ ↑x x_1)

instance PEquiv.instSemilatticeInfPEquiv {α : Type u} {β : Type v} [inst : DecidableEq α] [inst : DecidableEq β] :

SemilatticeInf (α ≃. β)

Equations

One or more equations did not get rendered due to their size.

def Equiv.toPEquiv {α : Type u_1} {β : Type u_2} (f : α ≃ β) :

α ≃. β

Turns an Equiv into a PEquiv of the whole type.

Equations

Equiv.toPEquiv f = { toFun := some ∘ ↑f, invFun := some ∘ ↑(Equiv.symm f), inv := (_ : ∀ (a : α) (a_1 : β), a ∈ some (↑(Equiv.symm f) a_1) ↔ a_1 ∈ some (↑f a)) }

@[simp]

theorem Equiv.toPEquiv_refl {α : Type u_1} :

Equiv.toPEquiv (Equiv.refl α) = PEquiv.refl α

theorem Equiv.toPEquiv_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α ≃ β) (g : β ≃ γ) :

Equiv.toPEquiv (Equiv.trans f g) = PEquiv.trans (Equiv.toPEquiv f) (Equiv.toPEquiv g)

theorem Equiv.toPEquiv_symm {α : Type u_1} {β : Type u_2} (f : α ≃ β) :

Equiv.toPEquiv (Equiv.symm f) = PEquiv.symm (Equiv.toPEquiv f)

theorem Equiv.toPEquiv_apply {α : Type u_1} {β : Type u_2} (f : α ≃ β) (x : α) :

↑(Equiv.toPEquiv f) x = some (↑f x)