Supporting results for pointwise provable equality.

noncomputable def PointwiseComposition.Classical.chooseUnique {α : Sort u_1} {p : α → Prop} (h : ∃! x : α, p x) : α

Choose the unique witness supplied by h.

Equations

• PointwiseComposition.Classical.chooseUnique h = Classical.choose ⋯

theorem PointwiseComposition.Classical.chooseUnique_spec {α : Sort u_1} {p : α → Prop} (h : ∃! x : α, p x) : p (chooseUnique h)

theorem PointwiseComposition.Classical.choose_uniq {α : Sort u_1} {p : α → Prop} {x : α} (h : ∃! x : α, p x) (hx : p x) : x = chooseUnique h

@[simp]

theorem PointwiseComposition.Classical.chooseUnique_eq_iff_right {α : Sort u_1} {p : α → Prop} {x : α} (h : ∃! x : α, p x) : x = chooseUnique h ↔ p x

@[simp]

theorem PointwiseComposition.Classical.chooseUnique_eq_iff_left {α : Sort u_1} {p : α → Prop} {x : α} (h : ∃! x : α, p x) : chooseUnique h = x ↔ p x

theorem PointwiseComposition.Classical.exitsUnique_extend {α : Sort u_1} {p : α → Prop} {r : α → α → Prop} (h : ∀ (x : α), p x → ∃! y : α, r x y) (default x : α) : ∃! y : α, (p x → r x y) ∧ (¬p x → y = default)

noncomputable def PointwiseComposition.Classical.extendedChooseUnique {α : Sort u_1} {p : α → Prop} {r : α → α → Prop} (h : ∀ (x : α), p x → ∃! y : α, r x y) (default x : α) : α

Choose the unique r-successor when p x holds, or return default otherwise.

Equations

• PointwiseComposition.Classical.extendedChooseUnique h default x = Classical.choose ⋯

theorem PointwiseComposition.Classical.extendedChooseUnique_spec {α : Sort u_1} {p : α → Prop} {r : α → α → Prop} {x : α} (h : ∀ (x : α), p x → ∃! y : α, r x y) (default : α) (hx : p x) : r x (extendedChooseUnique h default x)

theorem PointwiseComposition.Classical.extendedChooseUnique_spec_not {α : Sort u_1} {p : α → Prop} {r : α → α → Prop} {x : α} (h : ∀ (x : α), p x → ∃! y : α, r x y) (default : α) (hx : ¬p x) : extendedChooseUnique h default x = default

theorem PointwiseComposition.Classical.extendedChooseUnique_uniq {α : Sort u_1} {p : α → Prop} {r : α → α → Prop} {x y : α} (h : ∀ (x : α), p x → ∃! y : α, r x y) (default : α) (hpx : p x) (hrx : r x y) : y = extendedChooseUnique h default x

theorem PointwiseComposition.Classical.extendedChooseUnique_eq_iff {α : Sort u_1} {p : α → Prop} {r : α → α → Prop} {x y : α} (h : ∀ (x : α), p x → ∃! y : α, r x y) (default : α) (hpx : p x) : y = extendedChooseUnique h default x ↔ r x y