α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
g : β ≃. γ
a : α
⊢ (∀ (a_1 : γ), ¬∃ b, b ∈ ↑f a ∧ a_1 ∈ ↑g b) ↔ ∀ (b : β) (c : γ), b ∈ ↑f a → ¬c ∈ ↑g b
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
g : β ≃. γ
a : α
⊢ ↑(PEquiv.trans f g) a = none ↔ ∀ (b : β) (c : γ), ¬b ∈ ↑f a ∨ ¬c ∈ ↑g b
simp only [eq_none_iff_forall_not_mem, mem_trans, imp_iff_not_or.symm]
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
g : β ≃. γ
a : α
⊢ (∀ (a_1 : γ) (b : β), b ∈ ↑f a → ¬a_1 ∈ ↑g b) ↔ ∀ (b : β) (c : γ), b ∈ ↑f a → ¬c ∈ ↑g b
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
g : β ≃. γ
a : α
⊢ (∀ (a_1 : γ), ¬∃ b, b ∈ ↑f a ∧ a_1 ∈ ↑g b) ↔ ∀ (b : β) (c : γ), b ∈ ↑f a → ¬c ∈ ↑g b
push_neg
no goals
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
g : β ≃. γ
a : α
⊢ (∀ (a_1 : γ) (b : β), b ∈ ↑f a → ¬a_1 ∈ ↑g b) ↔ ∀ (b : β) (c : γ), b ∈ ↑f a → ¬c ∈ ↑g b
exact forall_swap