monotone_mem — Mathlib

English

For a fixed set s, the predicate x ↦ (x ∈ s) is monotone if and only if s is an upper set.

Русский

Для заданного множества s функция x ↦ (x ∈ s) является монотонной тогда и только тогда, когда s является верхним множеством.

LaTeX

$$$\operatorname{Monotone}(x \mapsto x \in s) \iff \operatorname{IsUpperSet}(s)$$$

Lean4

@[simp]
theorem monotone_mem : Monotone (· ∈ s) ↔ IsUpperSet s :=
  Iff.rfl

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