reflTransSymmAux_mem_I — Mathlib

English

The function reflTransSymmAux(t) lies in the unit interval for all t.

Русский

Функция reflTransSymmAux(t) принадлежит единичному интервалу для всех t.

LaTeX

$$$ reflTransSymmAux(t) \in I \quad \forall t \in I $$$

Lean4

theorem reflTransSymmAux_mem_I (x : I × I) : reflTransSymmAux x ∈ I :=
  by
  dsimp only [reflTransSymmAux]
  split_ifs
  · constructor
    · apply mul_nonneg
      · apply mul_nonneg
        · unit_interval
        · simp
      · unit_interval
    · rw [mul_assoc]
      apply mul_le_one₀
      · unit_interval
      · apply mul_nonneg
        · simp
        · unit_interval
      · linarith
  · constructor
    · apply mul_nonneg
      · unit_interval
      linarith [unitInterval.nonneg x.2, unitInterval.le_one x.2]
    · apply mul_le_one₀
      · unit_interval
      · linarith [unitInterval.nonneg x.2, unitInterval.le_one x.2]
      · linarith [unitInterval.nonneg x.2, unitInterval.le_one x.2]

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