mem_upperBounds_image_self — Mathlib

English

A simple corollary: if a ∈ lowerBounds t and a ∈ t, then f(a) ∈ upperBounds (f '' t) for an antitone f on t.

Русский

Следствие: если a принадлежит нижним границам t и t, то при антитонной f на t, f(a) лежит в верхних границах образа t.

LaTeX

$$$(Hf : AntitoneOn\ f\ t) : a \in lowerBounds(t) \\rightarrow a \in t \\rightarrow f(a) \in \mathrm{upperBounds}(\mathrm{image}(f,t))$$$

Lean4

theorem mem_upperBounds_image_self (Hf : AntitoneOn f t) : a ∈ lowerBounds t → a ∈ t → f a ∈ upperBounds (f '' t) :=
  Hf.dual_right.mem_lowerBounds_image_self

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