sigmaSigmaSubtype_symm_apply — Mathlib

English

The symmetric map of sigmaSigmaSubtype applied to c equals the element with a and b reconstructed by the witness h.

Русский

Симметричная карта sigmaSigmaSubtype при применении к c восстанавливает элементы a и b по свидетельству h.

LaTeX

$$$\\big( \\mathrm{sigmaSigmaSubtype}\\ p\\ h \\big)^{-1} c = \\langle \\langle a, \\langle b, c \\rangle \\rangle, h \\rangle$$$

Lean4

@[simp]
theorem sigmaSigmaSubtype_symm_apply {α : Type*} {β : α → Type*} {γ : (a : α) → β a → Type*} (p : (a : α) × β a → Prop)
    [uniq : Unique { ab // p ab }] {a : α} {b : β a} (c : γ a b) (h : p ⟨a, b⟩) :
    (sigmaSigmaSubtype p h).symm c = ⟨⟨a, ⟨b, c⟩⟩, h⟩ := by rw [Equiv.symm_apply_eq]; simp

Похожие утверждения