indepSets_congr — Mathlib

English

If κ =ᵐ[μ] η, then iIndepSets π κ μ ↔ iIndepSets π η μ.

Русский

Если κ =ᵐ[μ] η, то iIndepSets π κ μ ⇔ iIndepSets π η μ.

LaTeX

$$$κ =^m[μ] η \Rightarrow (iIndepSets\, π\, κ\, μ \iff iIndepSets\, π\, η\, μ)$$$

Lean4

theorem indepSets_congr (h : κ =ᵐ[μ] η) : IndepSets s1 s2 κ μ ↔ IndepSets s1 s2 η μ :=
  by
  peel 4
  refine ⟨fun h' ↦ ?_, fun h' ↦ ?_⟩ <;>
    · filter_upwards [h, h'] with a ha h'a
      simpa [ha] using h'a

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