theorem PartialEquiv.IsImage.restr_eq_restr_set {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) {s : Set α} {t : Set β} (h : e.IsImage s t) : h.restr = e.restr s

theorem PartialEquiv.image_subset_target {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) {s : Set α} (hs : s ⊆ e.source) : ↑e '' s ⊆ e.target

theorem PartialEquiv.symm_image_subset_source {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) {s : Set β} (hs : s ⊆ e.target) : ↑e.symm '' s ⊆ e.source

theorem PartialEquiv.image_isImage_of_subset_source {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) {s : Set α} (h : s ⊆ e.source) : e.IsImage s (↑e '' s)

theorem PartialEquiv.symm_image_isImage_of_subset_target {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) {s : Set β} (h : s ⊆ e.target) : e.IsImage (↑e.symm '' s) s

noncomputable def PartialEquiv.empty {α : Type u_1} {β : Type u_2} [Nonempty α] [Nonempty β] : PartialEquiv α β

The PartialEquiv with empty source and target. The types must be nonempty.

Equations

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

@[simp]

theorem PartialEquiv.empty_source {α : Type u_1} {β : Type u_2} [Nonempty α] [Nonempty β] : empty.source = ∅

@[simp]

theorem PartialEquiv.empty_target {α : Type u_1} {β : Type u_2} [Nonempty α] [Nonempty β] : empty.target = ∅

@[simp]

theorem PartialEquiv.empty_apply {α : Type u_1} {β : Type u_2} [Nonempty α] [Nonempty β] (x✝ : α) : ↑empty x✝ = Classical.arbitrary β

@[simp]

theorem PartialEquiv.empty_symm_apply {α : Type u_1} {β : Type u_2} [Nonempty α] [Nonempty β] (x✝ : β) : ↑empty.symm x✝ = Classical.arbitrary α

@[simp]

theorem PartialEquiv.symm_empty {α : Type u_1} {β : Type u_2} [Nonempty α] [Nonempty β] : empty.symm = empty

theorem Finite.exists_PartialEquiv_of_encard_eq {α : Type u_1} {β : Type u_2} [Nonempty α] [Nonempty β] {s : Set α} {t : Set β} (hfin : s.Finite) (h : s.encard = t.encard) : ∃ (e : PartialEquiv α β), e.source = s ∧ e.target = t

noncomputable def PartialEquiv.ofSetEquiv {α : Type u_1} {β : Type u_2} [Nonempty α] [Nonempty β] {s : Set α} {t : Set β} [DecidablePred fun (x : α) => x ∈ s] [DecidablePred fun (x : β) => x ∈ t] (e : ↑s ≃ ↑t) : PartialEquiv α β

Equations

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

@[simp]

theorem PartialEquiv.ofSetEquiv_symm_apply {α : Type u_1} {β : Type u_2} [Nonempty α] [Nonempty β] {s : Set α} {t : Set β} [DecidablePred fun (x : α) => x ∈ s] [DecidablePred fun (x : β) => x ∈ t] (e : ↑s ≃ ↑t) (y : β) : ↑(PartialEquiv.ofSetEquiv e).symm y = if h : y ∈ t then ↑(e.symm ⟨y, h⟩) else Classical.arbitrary α

@[simp]

theorem PartialEquiv.ofSetEquiv_source {α : Type u_1} {β : Type u_2} [Nonempty α] [Nonempty β] {s : Set α} {t : Set β} [DecidablePred fun (x : α) => x ∈ s] [DecidablePred fun (x : β) => x ∈ t] (e : ↑s ≃ ↑t) : (PartialEquiv.ofSetEquiv e).source = s

@[simp]

theorem PartialEquiv.ofSetEquiv_apply {α : Type u_1} {β : Type u_2} [Nonempty α] [Nonempty β] {s : Set α} {t : Set β} [DecidablePred fun (x : α) => x ∈ s] [DecidablePred fun (x : β) => x ∈ t] (e : ↑s ≃ ↑t) (x : α) : ↑(PartialEquiv.ofSetEquiv e) x = if h : x ∈ s then ↑(e ⟨x, h⟩) else Classical.arbitrary β

@[simp]

theorem PartialEquiv.ofSetEquiv_target {α : Type u_1} {β : Type u_2} [Nonempty α] [Nonempty β] {s : Set α} {t : Set β} [DecidablePred fun (x : α) => x ∈ s] [DecidablePred fun (x : β) => x ∈ t] (e : ↑s ≃ ↑t) : (PartialEquiv.ofSetEquiv e).target = t

@[simp]

theorem PartialEquiv.ofSetEquiv_apply_mem {α : Type u_1} {β : Type u_2} [Nonempty α] [Nonempty β] {s : Set α} {t : Set β} [DecidablePred fun (x : α) => x ∈ s] [DecidablePred fun (x : β) => x ∈ t] (e : ↑s ≃ ↑t) {x : α} (hx : x ∈ s) : ↑(PartialEquiv.ofSetEquiv e) x = ↑(e ⟨x, hx⟩)

def PartialEquiv.insert {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {a : α} {b : β} (e : PartialEquiv α β) (ha : a ∉ e.source) (hb : b ∉ e.target) : PartialEquiv α β

Extend the source/target of a PartialEquiv by setting e a = b.

Equations

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

@[simp]

theorem PartialEquiv.insert_target {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {a : α} {b : β} (e : PartialEquiv α β) (ha : a ∉ e.source) (hb : b ∉ e.target) : (e.insert ha hb).target = insert b e.target

@[simp]

theorem PartialEquiv.insert_source {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {a : α} {b : β} (e : PartialEquiv α β) (ha : a ∉ e.source) (hb : b ∉ e.target) : (e.insert ha hb).source = insert a e.source

@[simp]

theorem PartialEquiv.insert_apply {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {a : α} {b : β} (e : PartialEquiv α β) (ha : a ∉ e.source) (hb : b ∉ e.target) (a✝ : α) : ↑(e.insert ha hb) a✝ = Function.update (↑e) a b a✝

@[simp]

theorem PartialEquiv.insert_symm_apply {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {a : α} {b : β} (e : PartialEquiv α β) (ha : a ∉ e.source) (hb : b ∉ e.target) (a✝ : β) : ↑(e.insert ha hb).symm a✝ = Function.update (↑e.symm) b a a✝

theorem PartialEquiv.insert_apply_mem {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {a : α} {b : β} (e : PartialEquiv α β) (ha : a ∉ e.source) (hb : b ∉ e.target) {i : α} (hi : i ∈ e.source) : ↑(e.insert ha hb) i = ↑e i

@[simp]

theorem insert_symm {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {a : α} {b : β} (e : PartialEquiv α β) (ha : a ∉ e.source) (hb : b ∉ e.target) : (e.insert ha hb).symm = e.symm.insert hb ha

theorem PartialEquiv.insert_apply_symm_mem {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {a : α} {b : β} (e : PartialEquiv α β) (ha : a ∉ e.source) (hb : b ∉ e.target) {j : β} (hj : j ∈ e.target) : ↑(e.insert ha hb).symm j = ↑e.symm j

@[instance_reducible]

instance instPreorderPartialEquiv_matroid {α : Type u_3} {β : Type u_4} : Preorder (PartialEquiv α β)

φ ≤ φ' means that the source and target of φ are contained in those of φ', and that they agree on their common domain.

Equations

• instPreorderPartialEquiv_matroid = { le := fun (φ φ' : PartialEquiv α β) => φ.source ⊆ φ'.source ∧ ∀ {i : α}, i ∈ φ.source → ↑φ' i = ↑φ i, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

def Set.diffPartialEquiv {α : Type u_1} (s : Set α) : PartialEquiv (Set α) (Set α)

Equations

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

@[simp]

theorem Set.diffPartialEquiv_symm_apply {α : Type u_1} (s t : Set α) : ↑s.diffPartialEquiv.symm t = s \ t

@[simp]

theorem Set.diffPartialEquiv_target {α : Type u_1} (s : Set α) : s.diffPartialEquiv.target = Iic s

@[simp]

theorem Set.diffPartialEquiv_source {α : Type u_1} (s : Set α) : s.diffPartialEquiv.source = Iic s

@[simp]

theorem Set.diffPartialEquiv_apply {α : Type u_1} (s t : Set α) : ↑s.diffPartialEquiv t = s \ t