α : Type u_1
β : Type ?u.55845
σ : Type ?u.55848
τ : Type ?u.55851
f : Filter α
F : Realizer f
⊢ (∃ x, ¬Set.Nonempty (CFilter.f F.F x)) ↔ ∀ (b : Realizer.bot.σ), ∃ a, CFilter.f F.F a ≤ CFilter.f Realizer.bot.F b
α : Type u_1
β : Type ?u.55845
σ : Type ?u.55848
τ : Type ?u.55851
f : Filter α
F : Realizer f
⊢ f ≠ ⊥ ↔ ∀ (a : F.σ), Set.Nonempty (CFilter.f F.F a)
rw [not_iff_comm, ← le_bot_iff, F.le_iff Realizer.bot, not_forall]
α : Type u_1
β : Type ?u.55845
σ : Type ?u.55848
τ : Type ?u.55851
f : Filter α
F : Realizer f
⊢ (∃ x, CFilter.f F.F x = ∅) ↔ ∀ (b : Realizer.bot.σ), ∃ a, CFilter.f F.F a ≤ CFilter.f Realizer.bot.F b
α : Type u_1
β : Type ?u.55845
σ : Type ?u.55848
τ : Type ?u.55851
f : Filter α
F : Realizer f
⊢ (∃ x, ¬Set.Nonempty (CFilter.f F.F x)) ↔ ∀ (b : Realizer.bot.σ), ∃ a, CFilter.f F.F a ≤ CFilter.f Realizer.bot.F b
simp only [Set.not_nonempty_iff_eq_empty]
no goals
α : Type u_1
β : Type ?u.55845
σ : Type ?u.55848
τ : Type ?u.55851
f : Filter α
F : Realizer f
⊢ (∃ x, CFilter.f F.F x = ∅) ↔ ∀ (b : Realizer.bot.σ), ∃ a, CFilter.f F.F a ≤ CFilter.f Realizer.bot.F b
exact ⟨fun ⟨x, e⟩ _ ↦ ⟨x, le_of_eq e⟩, fun h ↦
  let ⟨x, h⟩ := h ()
  ⟨x, le_bot_iff.1 h⟩⟩