subtypeQuotientEquivQuotientSubtype_symm_mk

English

The inverse of subtypeQuotientEquivQuotientSubtype maps ⟦x⟧ to ⟨⟦x⟧, (hp₂ _).1 x.property⟩.

Русский

Обратное отображение subtypeQuotientEquivQuotientSubtype маппит ⟦x⟧ в ⟨⟦x⟧, (hp₂ _).1 x.property⟩.

LaTeX

$$$(subtypeQuotientEquivQuotientSubtype p₁ p₂ hp₂ h)^{-1} \\ ⟦x⟧ = ⟨⟦x⟧, (hp₂ _).1 x.property⟩$$$

Lean4

@[simp]
theorem subtypeQuotientEquivQuotientSubtype_symm_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) :
    (subtypeQuotientEquivQuotientSubtype p₁ p₂ hp₂ h).symm ⟦x⟧ = ⟨⟦x⟧, (hp₂ _).1 x.property⟩ :=
  rfl

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