of_subsingleton — Mathlib

English

Under a subsingleton index set, iIndepSets holds irrespective of the specific π, provided IsMarkovKernel κ.

Русский

При субодинонтенной множительности индексов iIndepSets выполняется независимо от конкретного π при условии, что κ — марковское ядро.

LaTeX

$$$ @[Subsingleton\\ ι] \\; iIndepSets m κ μ $$$

Lean4

@[nontriviality, simp]
theorem of_subsingleton [Subsingleton ι] {m : ι → Set (Set Ω)} {κ : Kernel α Ω} [IsMarkovKernel κ] : iIndepSets m κ μ :=
  by
  rintro s f hf
  obtain rfl | ⟨i, rfl⟩ : s = ∅ ∨ ∃ i, s = { i } := by
    simpa using (subsingleton_of_subsingleton (s := s.toSet)).eq_empty_or_singleton
  all_goals simp

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