subtype_toEquiv — Mathlib

English

If h: X ≃ₜ Y and h_iff relates p and q, then the induced subtype equivalence coincides with the original subtype equivalence.

Русский

Если h: X ≃ₜ Y и h_iff задаёт связь p и q, то полученное по подтипу эквивалентность совпадает с исходной подтиповой эквивалентностью.

LaTeX

$$$(h.subtype h\\_iff).toEquiv = h.toEquiv.subtypeEquiv h\\_iff$$$

Lean4

@[simp]
theorem subtype_toEquiv {p : X → Prop} {q : Y → Prop} (h : X ≃ₜ Y) (h_iff : ∀ x, p x ↔ q (h x)) :
    (h.subtype h_iff).toEquiv = h.toEquiv.subtypeEquiv h_iff :=
  rfl

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