mem_approxOrderOf_iff — Mathlib

English

For any A, n, δ, a ∈ approxOrderOf(A, n, δ) if and only if there exists b with orderOf(b) = n and a is within δ of b.

Русский

Для любых A, n, δ: a ∈ approxOrderOf(A, n, δ) тогда и только тогда существует b с orderOf(b) = n и a лежит в шаре вокруг b радиуса δ.

LaTeX

$$$$ a \in \operatorname{approxOrderOf}(A, n, δ) \iff \exists b: A, \operatorname{orderOf}(b) = n \land a \in B(b, δ). $$$$

Lean4

@[to_additive mem_approx_add_orderOf_iff]
theorem mem_approxOrderOf_iff {A : Type*} [SeminormedGroup A] {n : ℕ} {δ : ℝ} {a : A} :
    a ∈ approxOrderOf A n δ ↔ ∃ b : A, orderOf b = n ∧ a ∈ ball b δ := by
  simp only [approxOrderOf, thickening_eq_biUnion_ball, mem_iUnion₂, mem_setOf_eq, exists_prop]

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