Theorems · Theorem · general topology

Filter.le_div_iff

∀ {α : Type u_2} [inst : Div α] {f g h : Filter α}, h ≤ f / g ↔ ∀ ⦃s : Set α⦄, s ∈ f → ∀ ⦃t : Set α⦄, t ∈ g → s / t ∈ h

Defined in

Mathlib.Order.Filter.Pointwise

Cited by

2 results in Mathlib

Foundations

Depth 66 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Div