no goals
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Sort ?u.3746
π : α → Type ?u.3751
f : α → β
g : α → γ
g' : β → γ
⊢ restrict (range fᶜ) (extend f g g') = g' ∘ Subtype.val
classical
exact restrict_dite_compl _ _
no goals
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Sort ?u.3746
π : α → Type ?u.3751
f : α → β
g : α → γ
g' : β → γ
⊢ restrict (range fᶜ) (extend f g g') = g' ∘ Subtype.val
exact restrict_dite_compl _ _