no goals
α : Type u_1
β : Type ?u.4270
γ : Type ?u.4273
inst✝ : Fintype α
s t : Finset α
⊢ Codisjoint s t ↔ ∀ ⦃a : α⦄, ¬a ∈ s → a ∈ t
classical simp [codisjoint_iff, eq_univ_iff_forall, or_iff_not_imp_left]
no goals
α : Type u_1
β : Type ?u.4270
γ : Type ?u.4273
inst✝ : Fintype α
s t : Finset α
⊢ Codisjoint s t ↔ ∀ ⦃a : α⦄, ¬a ∈ s → a ∈ t
simp [codisjoint_iff, eq_univ_iff_forall, or_iff_not_imp_left]