Theorem: Sublattice.pi_bot (LeanCamCombi/Mathlib/Order/Sublattice.lean)

State before:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : Lattice α
inst✝³ : Lattice β
inst✝² : Lattice γ
L M : Sublattice α
f : LatticeHom α β
s t : Set α
a✝ : α
κ : Type u_5
π : κ → Type u_6
inst✝¹ : (i : κ) → Lattice (π i)
inst✝ : Nonempty κ
a : (i : κ) → π i
⊢ (a ∈ pi univ fun i => ⊥) ↔ a ∈ ⊥
Tactic:
simp [mem_pi]
State after:
no goals