setCongr — Mathlib

English

If two subsets s and t of α are equal, then their corresponding subtype sets are equivalent.

Русский

Если два подмножества s и t ⊆ α равны, то их соответствующие подтипы эквивалентны.

LaTeX

$$$ s = t \Rightarrow s^E \simeq t^E $$$

Lean4

/-- The subtypes corresponding to equal sets are equivalent. -/
@[simps! apply symm_apply]
def setCongr {α : Type*} {s t : Set α} (h : s = t) : s ≃ t :=
  subtypeEquivProp h

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