case h
α : Type u_1
β : Type u_2
γ : Type ?u.1354
r : Rel α β
x : α
⊢ x ∈ codom (inv r) ↔ x ∈ dom r
α : Type u_1
β : Type u_2
γ : Type ?u.1354
r : Rel α β
⊢ codom (inv r) = dom r
ext x
no goals
case h
α : Type u_1
β : Type u_2
γ : Type ?u.1354
r : Rel α β
x : α
⊢ x ∈ codom (inv r) ↔ x ∈ dom r
rfl