mem_rangeIcc_apply_iff — Mathlib

English

An element a belongs to f.rangeIcc g at index i iff a lies between f(i) and g(i) in the coordinate order.

Русский

Элемент a принадлежит f.rangeIcc g на позиции i тогда и только тогда, когда a лежит между f(i) и g(i) по координатному порядку.

LaTeX

$$a ∈ f.rangeIcc g i ↔ f i ≤ a ∧ a ≤ g i$$

Lean4

theorem mem_rangeIcc_apply_iff : a ∈ f.rangeIcc g i ↔ f i ≤ a ∧ a ≤ g i :=
  mem_Icc

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