mathlib3
87439b98 - chore(logic/basic): add `forall_apply_eq_imp_iff₂` (#5072)

Commit

5 years ago

chore(logic/basic): add `forall_apply_eq_imp_iff₂` (#5072) Other lemmas simplify `∀ y ∈ f '' s, p y` to the LHS of this lemma.

Author

urkud

Parents