case a
α : Type ?u.100123
β : Type ?u.100126
γ : Type ?u.100129
n : ℕ
i m : Fin (n + 1)
⊢ m ∈ image (↑(succAbove i)) univ ↔ m ∈ {i}ᶜ
α : Type ?u.100123
β : Type ?u.100126
γ : Type ?u.100129
n : ℕ
i : Fin (n + 1)
⊢ image (↑(succAbove i)) univ = {i}ᶜ
ext m
no goals
case a
α : Type ?u.100123
β : Type ?u.100126
γ : Type ?u.100129
n : ℕ
i m : Fin (n + 1)
⊢ m ∈ image (↑(succAbove i)) univ ↔ m ∈ {i}ᶜ
simp