subtypeQuotientEquivQuotientSubtype_mk

English

There is a canonical equivalence between a subtype with a proof hx and the corresponding quotient element ⟨⟦x⟧, hx⟩.

Русский

Существует каноническая эквивалентность между подтипом с доказательством hx и соответствующим элементом частоты ⟨⟦x⟧, hx⟩.

LaTeX

$$$(subtypeQuotientEquivQuotientSubtype p₁ p₂ hp₂ h) \\ ⟨⟦x⟧, hx⟩ = ⟦⟨x, (hp₂ _).2 hx⟩⟧$$$

Lean4

@[simp]
theorem subtypeQuotientEquivQuotientSubtype_mk (p₁ : α → Prop) [s₁ : Setoid α] [s₂ : Setoid (Subtype p₁)]
    (p₂ : Quotient s₁ → Prop) (hp₂ : ∀ a, p₁ a ↔ p₂ ⟦a⟧) (h : ∀ x y : Subtype p₁, s₂ x y ↔ (x : α) ≈ y) (x hx) :
    subtypeQuotientEquivQuotientSubtype p₁ p₂ hp₂ h ⟨⟦x⟧, hx⟩ = ⟦⟨x, (hp₂ _).2 hx⟩⟧ :=
  rfl

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