noncomputable def allOnesOperator : EuclideanSpace ℝ (Fin 2) →L[ℝ] EuclideanSpace ℝ (Fin 2)

The bounded linear operator on ℝ² induced by the matrix [[1, 1], [1, 1]].

noncomputable def firstCoordinateProjector : EuclideanSpace ℝ (Fin 2) →L[ℝ] EuclideanSpace ℝ (Fin 2)

The bounded linear operator on ℝ² induced by the matrix [[1, 0], [0, 0]].

noncomputable def quarterTurnOperator : EuclideanSpace ℝ (Fin 2) →L[ℝ] EuclideanSpace ℝ (Fin 2)

The bounded linear operator on ℝ² induced by the quarter-turn matrix [[0, -1], [1, 0]].

theorem allOnesOperator_isMonotone : (↑allOnesOperator).IsMonotone

Example 20.19 (1): the operator A = [[1, 1], [1, 1]] is monotone on ℝ².

theorem firstCoordinateProjector_isMonotone : (↑firstCoordinateProjector).IsMonotone

Example 20.19 (2): the operator B = [[1, 0], [0, 0]] is monotone on ℝ².

theorem quarterTurnOperator_isMonotone : (↑quarterTurnOperator).IsMonotone

Example 20.19 (3): the operator C = [[0, -1], [1, 0]] is monotone on ℝ².

theorem neg_quarterTurnOperator_isMonotone : (↑(-quarterTurnOperator)).IsMonotone

Example 20.19 (4): the operator -C is monotone on ℝ².

theorem allOnesOperator_mul_firstCoordinateProjector_not_isMonotone : ¬(↑(allOnesOperator * firstCoordinateProjector)).IsMonotone

Example 20.19 (5): the product AB need not be monotone, showing that the hypotheses of Fact 20.18 cannot be dropped.

theorem quarterTurnOperator_sq_not_isMonotone : ¬(↑(quarterTurnOperator ^ 2)).IsMonotone

Example 20.19 (6): the square C^2 is not monotone, again showing that the hypotheses of Fact 20.18 are essential.