Theorems · Definition · general topology

Filter.Germ.LiftRel

{α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → {l : Filter α} → (β → γ → Prop) → l.Germ β → l.Germ γ → Prop

Lift a relation r : β → γ → Prop to Germ l β → Germ l γ → Prop.

Defined in

Mathlib.Order.Filter.Germ.Basic

Cited by

5 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext, Quot.sound