iIndepSets_congr — Mathlib

English

If kernels κ and η are equal μ-almost everywhere, then iIndepSets π κ μ ↔ iIndepSets π η μ.

Русский

Если ядра κ и η совпадают почти повсеместно по μ, то iIndepSets π κ μ ⇔ iIndepSets π η μ.

LaTeX

$$$\kappa =^a_e\!_μ \eta \Rightarrow (iIndepSets\, π\, κ\, μ \iff iIndepSets\, π\, η\, μ)$$$

Lean4

theorem iIndepSets_congr (h : κ =ᵐ[μ] η) : iIndepSets π κ μ ↔ iIndepSets π η μ :=
  by
  peel 3
  refine ⟨fun h' ↦ ?_, fun h' ↦ ?_⟩ <;>
    · filter_upwards [h, h'] with a ha h'a
      simpa [ha] using h'a

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