Theorems · Theorem · general topology

Filter.rcomap_rcomap

∀ {α : Type u} {β : Type v} {γ : Type w} (r : SetRel α β) (s : SetRel β γ) (l : Filter γ),
  Filter.rcomap r (Filter.rcomap s l) = Filter.rcomap (r.comp s) l

Defined in

Mathlib.Order.Filter.Partial

Cited by

1 results in Mathlib

Foundations

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