α : Type u_2
β : Type u_1
γ : Type ?u.63472
inst✝ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b c : β
⊢ (∃ a, a ∈ s ∧ const α b a = c) ↔ Finset.Nonempty s ∧ b = c
α : Type u_2
β : Type u_1
γ : Type ?u.63472
inst✝ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b c : β
⊢ c ∈ image (const α b) s ↔ Finset.Nonempty s ∧ b = c
rw [mem_image]
α : Type u_2
β : Type u_1
γ : Type ?u.63472
inst✝ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b c : β
⊢ (∃ x, x ∈ s) ∧ b = c ↔ Finset.Nonempty s ∧ b = c
α : Type u_2
β : Type u_1
γ : Type ?u.63472
inst✝ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b c : β
⊢ (∃ a, a ∈ s ∧ const α b a = c) ↔ Finset.Nonempty s ∧ b = c
simp only [exists_prop, const_apply, exists_and_right]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.63472
inst✝ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b c : β
⊢ (∃ x, x ∈ s) ∧ b = c ↔ Finset.Nonempty s ∧ b = c
rfl