directedOn_range — Mathlib

English

A subset is r-directed along a range if and only if it is directed with respect to the preimage relation along the domain.

Русский

Подмножество является направленным по отношению r к образу, если и только если оно направлено по отношению r к предобразу через соответствующую карту.

LaTeX

$$$Directed\\ r\\ f \\leftrightarrow DirectedOn\\ r\\ (Set.range\\ f)$$$

Lean4

theorem directedOn_range {f : ι → α} : Directed r f ↔ DirectedOn r (Set.range f) := by
  simp_rw [Directed, DirectedOn, Set.forall_mem_range, Set.exists_range_iff]

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