← Mathematical handbook

theorem Verification.n21Comparison_inv {θ η : ℝ} (hθ : 1 ≤ θ) (hη : 1 ≤ η) (u : ↑unitInterval) : n21Comparison θ η ((n21Generator θ hθ).invFun u) = (n21Generator η hη).invFun u

theorem Verification.n21Comparison_psi {θ η t : ℝ} (hθ : 1 ≤ θ) (hη : 1 ≤ η) (ht : t ∈ Set.Icc 0 1) : n21Psi η (n21Comparison θ η t) = n21Psi θ t

theorem Verification.nelsen21_lowerOrthant_monotone {θ η : ℝ} (hθ : 1 ≤ θ) (hθη : θ ≤ η) : (nelsen21 θ hθ).LowerOrthantLE (nelsen21 η ⋯)