directedOn_image — Mathlib

English

Let r be a relation on α, s ⊆ β, and f: β → α. Then DirectedOn r (image f s) is equivalent to DirectedOn (Order.Preimage f r) s.

Русский

Пусть r — отношение на α, s ⊆ β и f: β → α. Тогда DirectedOn r (образ f на s) эквивалентно DirectedOn (Order.Preimage f r) s.

LaTeX

$$$DirectedOn\\ r\\ (Set.image f\\ s) \\iff DirectedOn\\ (Order.Preimage f\\ r)\\ s$$$

Lean4

theorem directedOn_image {s : Set β} {f : β → α} : DirectedOn r (f '' s) ↔ DirectedOn (f ⁻¹'o r) s := by
  simp only [DirectedOn, Set.mem_image, exists_exists_and_eq_and, forall_exists_index, and_imp,
    forall_apply_eq_imp_iff₂, Order.Preimage]

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