α : Type u_2
α' : Type ?u.23464
β : Type u_3
β' : Type ?u.23470
γ : Type u_1
γ' : Type ?u.23476
δ : Type ?u.23479
δ' : Type ?u.23482
ε : Type ?u.23485
ε' : Type ?u.23488
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
⊢ map₂ m f g ≠ ⊥ ↔ f ≠ ⊥ ∧ g ≠ ⊥
α : Type u_2
α' : Type ?u.23464
β : Type u_3
β' : Type ?u.23470
γ : Type u_1
γ' : Type ?u.23476
δ : Type ?u.23479
δ' : Type ?u.23482
ε : Type ?u.23485
ε' : Type ?u.23488
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
⊢ NeBot (map₂ m f g) ↔ NeBot f ∧ NeBot g
simp_rw [neBot_iff]
no goals
α : Type u_2
α' : Type ?u.23464
β : Type u_3
β' : Type ?u.23470
γ : Type u_1
γ' : Type ?u.23476
δ : Type ?u.23479
δ' : Type ?u.23482
ε : Type ?u.23485
ε' : Type ?u.23488
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
⊢ map₂ m f g ≠ ⊥ ↔ f ≠ ⊥ ∧ g ≠ ⊥
exact map₂_eq_bot_iff.not.trans not_or