Mathlib.Algebra.Notation.Lemmas

one_le_dite theorem

[LE α] (ha : ∀ h, 1 ≤ a h) (hb : ∀ h, 1 ≤ b h) : 1 ≤ dite p a b

Full source

@[to_additive dite_nonneg]
lemma one_le_dite [LE α] (ha : ∀ h, 1 ≤ a h) (hb : ∀ h, 1 ≤ b h) : 1 ≤ dite p a b := by
  split; exacts [ha ‹_›, hb ‹_›]

One is Less Than or Equal to Dependent If-Then-Else Expression

Informal description

Let $\alpha$ be a type with a less-than-or-equal relation $\leq$. For any predicate $p$ and functions $a, b$ from the truth value of $p$ to $\alpha$, if $1 \leq a(h)$ for all $h$ and $1 \leq b(h)$ for all $h$, then $1 \leq \text{dite}(p, a, b)$, where $\text{dite}(p, a, b)$ is the dependent if-then-else expression that evaluates to $a(\text{proof of }p)$ if $p$ is true and $b(\text{proof of }\neg p)$ otherwise.

dite_le_one theorem

[LE α] (ha : ∀ h, a h ≤ 1) (hb : ∀ h, b h ≤ 1) : dite p a b ≤ 1

Full source

@[to_additive]
lemma dite_le_one [LE α] (ha : ∀ h, a h ≤ 1) (hb : ∀ h, b h ≤ 1) : dite p a b ≤ 1 := by
  split; exacts [ha ‹_›, hb ‹_›]

Dependent If-Then-Else Expression is Bounded Above by One

Informal description

Let $\alpha$ be a type with a binary relation $\leq$ (denoted by `[LE α]`). For any predicate $p$ and functions $a, b$ from the truth value of $p$ to $\alpha$, if $a(h) \leq 1$ for all $h$ where $p$ holds and $b(h) \leq 1$ for all $h$ where $\neg p$ holds, then the value of the dependent if-then-else expression $\mathrm{dite}(p, a, b)$ is less than or equal to $1$.

one_lt_dite theorem

[LT α] (ha : ∀ h, 1 < a h) (hb : ∀ h, 1 < b h) : 1 < dite p a b

Full source

@[to_additive dite_pos]
lemma one_lt_dite [LT α] (ha : ∀ h, 1 < a h) (hb : ∀ h, 1 < b h) : 1 < dite p a b := by
  split; exacts [ha ‹_›, hb ‹_›]

One is Less Than Dependent If-Then-Else Expression

Informal description

Let $\alpha$ be a type with a strict order relation $<$. For any predicate $p$ and functions $a, b$ from the proof of $p$ (or $\neg p$) to $\alpha$, if for all proofs $h$ of $p$ we have $1 < a(h)$ and for all proofs $h$ of $\neg p$ we have $1 < b(h)$, then $1$ is less than the dependent if-then-else expression $\mathrm{dite}(p, a, b)$.

dite_lt_one theorem

[LT α] (ha : ∀ h, a h < 1) (hb : ∀ h, b h < 1) : dite p a b < 1

Full source

@[to_additive]
lemma dite_lt_one [LT α] (ha : ∀ h, a h < 1) (hb : ∀ h, b h < 1) : dite p a b < 1 := by
  split; exacts [ha ‹_›, hb ‹_›]

Dependent If-Then-Else Expression is Less Than One

Informal description

Let $\alpha$ be a type with a strict order relation $<$. For any predicate $p$ and functions $a, b$ from the truth value of $p$ to $\alpha$, if $a(h) < 1$ and $b(h) < 1$ for all $h$, then the dependent if-then-else expression $\mathrm{dite}(p, a, b) < 1$.

one_le_ite theorem

[LE α] (ha : 1 ≤ a) (hb : 1 ≤ b) : 1 ≤ ite p a b

Full source

@[to_additive ite_nonneg]
lemma one_le_ite [LE α] (ha : 1 ≤ a) (hb : 1 ≤ b) : 1 ≤ ite p a b := by split <;> assumption

Lower Bound Preservation under Conditional Choice: $1 \leq \text{ite}(p, a, b)$

Informal description

Let $α$ be a type with a less-than-or-equal-to relation $\leq$. For any boolean condition $p$ and elements $a, b \in α$ such that $1 \leq a$ and $1 \leq b$, we have $1 \leq \text{ite}(p, a, b)$, where $\text{ite}(p, a, b)$ denotes the element $a$ if $p$ is true and $b$ otherwise.

ite_le_one theorem

[LE α] (ha : a ≤ 1) (hb : b ≤ 1) : ite p a b ≤ 1

Full source

@[to_additive]
lemma ite_le_one [LE α] (ha : a ≤ 1) (hb : b ≤ 1) : ite p a b ≤ 1 := by split <;> assumption

Conditional Expression Bounded Above by One

Informal description

For any type $\alpha$ with a less-than-or-equal-to relation $\leq$, and for any elements $a, b \in \alpha$ such that $a \leq 1$ and $b \leq 1$, the conditional expression $\text{ite}(p, a, b)$ (which evaluates to $a$ if $p$ is true and $b$ otherwise) satisfies $\text{ite}(p, a, b) \leq 1$.

one_lt_ite theorem

[LT α] (ha : 1 < a) (hb : 1 < b) : 1 < ite p a b

Full source

@[to_additive ite_pos]
lemma one_lt_ite [LT α] (ha : 1 < a) (hb : 1 < b) : 1 < ite p a b := by split <;> assumption

Conditional Expression Preserves Strict Inequality with One

Informal description

Let $\alpha$ be a type with a strict order relation $<$, and let $a, b \in \alpha$ such that $1 < a$ and $1 < b$. Then for any proposition $p$, the value of the conditional expression $\text{ite}(p, a, b)$ (which equals $a$ if $p$ is true and $b$ otherwise) satisfies $1 < \text{ite}(p, a, b)$.

ite_lt_one theorem

[LT α] (ha : a < 1) (hb : b < 1) : ite p a b < 1

Full source

@[to_additive]
lemma ite_lt_one [LT α] (ha : a < 1) (hb : b < 1) : ite p a b < 1 := by split <;> assumption

Conditional Term Less Than One

Informal description

Let $\alpha$ be a type with a strict order relation $<$, and let $a, b \in \alpha$ be elements such that $a < 1$ and $b < 1$. Then for any proposition $p$, the term $\text{ite}(p, a, b)$ (which equals $a$ if $p$ is true and $b$ otherwise) satisfies $\text{ite}(p, a, b) < 1$.