Supporting results for pointwise provable equality.

class PointwiseComposition.FFL.FirstOrder.Tarski.Structure.Monotone (L : Language) (M : Type u_1) [LE M] [Structure L M] : Prop

Data and laws for Monotone in FFL.FirstOrder.Tarski.Structure.

• monotone {k : ℕ} (f : L.Func k) (v₁ v₂ : Fin k → M) : (∀ (i : Fin k), v₁ i ≤ v₂ i) → func f v₁ ≤ func f v₂

theorem PointwiseComposition.FFL.FirstOrder.Tarski.Structure.Monotone.term_monotone {L : Language} {M : Type u_1} [LE M] [Structure L M] [Monotone L M] {ξ : Type u_2} {n : ℕ} (t : Semiterm L ξ n) {fv₁ fv₂ : Fin n → M} {bv₁ bv₂ : ξ → M} (he : ∀ (i : Fin n), fv₁ i ≤ fv₂ i) (hε : ∀ (i : ξ), bv₁ i ≤ bv₂ i) : Semiterm.val fv₁ bv₁ t ≤ Semiterm.val fv₂ bv₂ t