directedOn_iff_directed — Mathlib

English

For any relation r, a set s is DirectedOn r s if and only if the image of s under the inclusion map is Directed.

Русский

Для любой связи r множество s является DirectedOn r s тогда, когда образ этого множества под включением является Directed.

LaTeX

$$$\text{DirectedOn } r\ s \;\iff\; \text{Directed } r \ (\mathrm{Subtype.val} : s \to α)$$$

Lean4

theorem directedOn_iff_directed {s} : @DirectedOn α r s ↔ Directed r (Subtype.val : s → α) :=
  by
  simp only [DirectedOn, Directed, Subtype.exists, exists_and_left, exists_prop, Subtype.forall]
  exact forall₂_congr fun x _ => by simp [And.comm, and_assoc]

Похожие утверждения