le_einfsep_image_iff — Mathlib

English

For function f: β → α and set s ⊆ β, d ≤ einfsep (f '' s) holds iff ∀ x ∈ s, ∀ y ∈ s, f x ≠ f y → d ≤ edist (f x) (f y).

Русский

Для функции f: β → α и множества s ⊆ β, выполняется неравенство d ≤ einfsep(f''s) тогда и только тогда, когда для любых x,y ∈ s различаются по значению f x ≠ f y и d ≤ edist (f x) (f y).

LaTeX

$$$d \le einfsep (f '' s) \iff \forall x \in s, \forall y \in s, f x \neq f y \rightarrow d \le edist (f x) (f y)$$$

Lean4

theorem le_einfsep_image_iff {d} {f : β → α} {s : Set β} :
    d ≤ einfsep (f '' s) ↔ ∀ x ∈ s, ∀ y ∈ s, f x ≠ f y → d ≤ edist (f x) (f y) := by
  simp_rw [le_einfsep_iff, forall_mem_image]

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