English
A subtype of a sum is equivalent to a sum of subtypes: {c // p c} ≃ {a // p (Sum.inl a)} ⊕ {b // p (Sum.inr b)}.
Русский
Подтип суммы эквивалентен сумме подтипов: {c // p c} ≃ {a // p (Sum.inl a)} ⊕ {b // p (Sum.inr b)}.
LaTeX
$$def subtypeSum {α β} {p : α ⊕ β → Prop} : { c // p c } ≃ { a // p (Sum.inl a) } ⊕ { b // p (Sum.inr b) }$$
Lean4
/-- A subtype of a sum is equivalent to a sum of subtypes. -/
def subtypeSum {α β} {p : α ⊕ β → Prop} : { c // p c } ≃ { a // p (Sum.inl a) } ⊕ { b // p (Sum.inr b) }
where
toFun
| ⟨.inl a, h⟩ => .inl ⟨a, h⟩
| ⟨.inr b, h⟩ => .inr ⟨b, h⟩
invFun
| .inl a => ⟨.inl a, a.2⟩
| .inr b => ⟨.inr b, b.2⟩
left_inv := by rintro ⟨a | b, h⟩ <;> rfl
right_inv := by rintro (a | b) <;> rfl
