mem_accumulate — Mathlib

English

Let z ∈ β. Then z ∈ Accumulate s x if and only if there exists y ≤ x with z ∈ s(y).

Русский

Пусть z ∈ β. Тогда z ∈ Accumulate s x тогда и только тогда, когда существует y ≤ x и z ∈ s(y).

LaTeX

$$$z \\in \\mathrm{Accumulate}(s,x) \\iff \\exists y \\le x,\\ z \\in s(y)$$$

Lean4

@[simp]
theorem mem_accumulate [LE α] {x : α} {z : β} : z ∈ Accumulate s x ↔ ∃ y ≤ x, z ∈ s y := by
  simp_rw [accumulate_def, mem_iUnion₂, exists_prop]

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