Theorems · Theorem · order theory

DirectedOn.fst

∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r₂ : β → β → Prop} {d : Set (α × β)},
  DirectedOn (fun p q => r p.1 q.1 ∧ r₂ p.2 q.2) d → DirectedOn (fun x1 x2 => r x1 x2) (Prod.fst '' d)

Defined in

Mathlib.Order.Directed

Cited by

1 results in Mathlib

Foundations

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