P : Type u_1
inst✝ : CompleteSemilatticeInf P
F✝ : PFilter P
x : P
F : (PFilter P)ᵒᵈ
⊢ ↑toDual (principal x) ≤ F ↔ ∀ (b : P), b ∈ ↑ofDual F → x ≤ b
P : Type u_1
inst✝ : CompleteSemilatticeInf P
F✝ : PFilter P
x : P
F : (PFilter P)ᵒᵈ
⊢ (fun x => ↑toDual (principal x)) x ≤ F ↔ x ≤ (fun F => sInf ↑(↑ofDual F)) F
simp
no goals
P : Type u_1
inst✝ : CompleteSemilatticeInf P
F✝ : PFilter P
x : P
F : (PFilter P)ᵒᵈ
⊢ ↑toDual (principal x) ≤ F ↔ ∀ (b : P), b ∈ ↑ofDual F → x ≤ b
rfl