LeanMachineLearning exposition

ProbabilityTheory.Kernel.le_iff🔗

Minimal Lean file

le_iff🔗

LemmaProbabilityTheory.Kernel.le_iff
Details

No docstring.

🔗theorem
ProbabilityTheory.Kernel.le_iff.{u_1, u_2} {α : Type u_1} {β : Type u_2}
  {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ η : Kernel α β) :
  κ ≤ η ↔ ∀ (a : α), κ a ≤ η a
ProbabilityTheory.Kernel.le_iff.{u_1, u_2}
  {α : Type u_1} {β : Type u_2}
  {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  (κ η : Kernel α β) :
  κ ≤ η ↔ ∀ (a : α), κ a ≤ η a

Code

lemma le_iff (κ η : Kernel α β) : κ ≤ η ↔ ∀ a, κ a ≤ η a
Used by (2)

Actions: Source · Open Issue

Proof
Iff.rfl