Conversion between set-based notions and type-based notions

These conversions are frequently used throughout the project.

def HasSubset.Subset.elem {α : Type u_1} {X Y : Set α} (hXY : X ⊆ Y) (x : ↑X) : ↑Y

Given X ⊆ Y cast an element of X as an element of Y.

Equations

• hXY.elem x = ⟨↑x, ⋯⟩

theorem HasSubset.Subset.elem_range {α : Type u_1} {X Y : Set α} (hXY : X ⊆ Y) : hXY.elem.range = {a : ↑Y | ↑a ∈ X}

theorem HasSubset.Subset.elem_injective {α : Type u_1} {X Y : Set α} (hXY : X ⊆ Y) : Function.Injective hXY.elem

@[reducible, inline]

abbrev HasSubset.Subset.embed {α : Type u_1} {X Y : Set α} (hXY : X ⊆ Y) : ↑X ↪ ↑Y

Given X ⊆ Y provide an embedding (i.e., bundled injective function) from X into Y.

Equations

• hXY.embed = { toFun := hXY.elem, inj' := ⋯ }

def Subtype.toSum {α : Type u_1} {X Y : Set α} [(a : α) → Decidable (a ∈ X)] [(a : α) → Decidable (a ∈ Y)] (i : ↑(X ∪ Y)) : ↑X ⊕ ↑Y

Convert (X ∪ Y).Elem to X.Elem ⊕ Y.Elem.

Equations

• i.toSum = if hiX : ↑i ∈ X then ◩⟨↑i, hiX⟩ else if hiY : ↑i ∈ Y then ◪⟨↑i, hiY⟩ else ⋯.elim

def Subtype.toSum_unexpand : Lean.PrettyPrinter.Unexpander

Equations

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

@[simp]

theorem toSum_left {α : Type u_1} {X Y : Set α} [(a : α) → Decidable (a ∈ X)] [(a : α) → Decidable (a ∈ Y)] {x : ↑(X ∪ Y)} (hx : ↑x ∈ X) : x.toSum = ◩⟨↑x, hx⟩

@[simp]

theorem toSum_right {α : Type u_1} {X Y : Set α} [(a : α) → Decidable (a ∈ X)] [(a : α) → Decidable (a ∈ Y)] {y : ↑(X ∪ Y)} (hyX : ↑y ∉ X) (hyY : ↑y ∈ Y) : y.toSum = ◪⟨↑y, hyY⟩

theorem val_eq_val_of_toSum_eq_left {α : Type u_1} {X Y : Set α} [(a : α) → Decidable (a ∈ X)] [(a : α) → Decidable (a ∈ Y)] {x : ↑X} {x' : ↑(X ∪ Y)} (hxx : x'.toSum = ◩x) : ↑x = ↑x'

theorem val_eq_val_of_toSum_eq_right {α : Type u_1} {X Y : Set α} [(a : α) → Decidable (a ∈ X)] [(a : α) → Decidable (a ∈ Y)] {y : ↑Y} {y' : ↑(X ∪ Y)} (hyy : y'.toSum = ◪y) : ↑y = ↑y'

def Sum.toUnion {α : Type u_1} {X Y : Set α} (i : ↑X ⊕ ↑Y) : ↑(X ∪ Y)

Convert X.Elem ⊕ Y.Elem to (X ∪ Y).Elem.

Equations

• i.toUnion = Sum.casesOn i ⋯.elem ⋯.elem

@[simp]

theorem toUnion_left {α : Type u_1} {X Y : Set α} (x : ↑X) : (◩x).toUnion = ⟨↑x, ⋯⟩

@[simp]

theorem toUnion_right {α : Type u_1} {X Y : Set α} (y : ↑Y) : (◪y).toUnion = ⟨↑y, ⋯⟩

@[simp]

theorem toSum_toUnion {α : Type u_1} {X Y : Set α} [(a : α) → Decidable (a ∈ X)] [(a : α) → Decidable (a ∈ Y)] (i : ↑(X ∪ Y)) : i.toSum.toUnion = i

Converting (X ∪ Y).Elem to X.Elem ⊕ Y.Elem and back to (X ∪ Y).Elem gives the original element.

@[simp]

theorem toUnion_toSum {α : Type u_1} {X Y : Set α} [(a : α) → Decidable (a ∈ X)] [(a : α) → Decidable (a ∈ Y)] (hXY : X ⫗ Y) (i : ↑X ⊕ ↑Y) : i.toUnion.toSum = i

Converting X.Elem ⊕ Y.Elem to (X ∪ Y).Elem and back to X.Elem ⊕ Y.Elem gives the original element, assuming that X and Y are disjoint.

def Disjoint.equivSumUnion {α : Type u_1} {X Y : Set α} [(a : α) → Decidable (a ∈ X)] [(a : α) → Decidable (a ∈ Y)] (hXY : X ⫗ Y) : ↑X ⊕ ↑Y ≃ ↑(X ∪ Y)

Equivalence between X.Elem ⊕ Y.Elem and (X ∪ Y).Elem (i.e., a bundled bijection).

Equations

• hXY.equivSumUnion = { toFun := Sum.toUnion, invFun := Subtype.toSum, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem equivSumUnion_apply_left {α : Type u_1} {X Y : Set α} [(a : α) → Decidable (a ∈ X)] [(a : α) → Decidable (a ∈ Y)] (hXY : X ⫗ Y) (x : ↑X) : hXY.equivSumUnion ◩x = ⟨↑x, ⋯⟩

@[simp]

theorem equivSumUnion_apply_right {α : Type u_1} {X Y : Set α} [(a : α) → Decidable (a ∈ X)] [(a : α) → Decidable (a ∈ Y)] (hXY : X ⫗ Y) (y : ↑Y) : hXY.equivSumUnion ◪y = ⟨↑y, ⋯⟩

@[simp]

theorem equivSumUnion_symm_apply_left {α : Type u_1} {X Y : Set α} [(a : α) → Decidable (a ∈ X)] [(a : α) → Decidable (a ∈ Y)] (hXY : X ⫗ Y) {x : ↑(X ∪ Y)} (hx : ↑x ∈ X) : hXY.equivSumUnion.symm x = ◩⟨↑x, hx⟩

@[simp]

theorem equivSumUnion_symm_apply_right {α : Type u_1} {X Y : Set α} [(a : α) → Decidable (a ∈ X)] [(a : α) → Decidable (a ∈ Y)] (hXY : X ⫗ Y) {y : ↑(X ∪ Y)} (hy : ↑y ∈ Y) : hXY.equivSumUnion.symm y = ◪⟨↑y, hy⟩