disjoint_partialSups_right — Mathlib

English

Let f: ι → α, i ∈ ι, and x ∈ α. Then x is disjoint from partialSups f i if and only if x is disjoint from every f(j) with j ≤ i.

Русский

Пусть f: ι → α, i ∈ ι, и x ∈ α. Тогда x несовпадает с partialSups f i тогда и только тогда x не пересекается с каждым f(j) при j ≤ i.

LaTeX

$$$\operatorname{Disjoint}\big(x,\operatorname{partialSups} f\, i\big) \iff \forall j \le i,\; \operatorname{Disjoint}\big(x, f(j)\big)$$$

Lean4

@[simp]
theorem disjoint_partialSups_right {f : ι → α} {i : ι} {x : α} :
    Disjoint x (partialSups f i) ↔ ∀ j ≤ i, Disjoint x (f j) :=
  partialSups_iff_forall (Disjoint x) disjoint_sup_right

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