rank_congr — Mathlib

English

If two pre-sets x and y are equivalent, then their ranks are equal.

Русский

Если два пред-множества x и y эквивалентны, тогда их ранги равны.

LaTeX

$$$$ x \cong y \Rightarrow \operatorname{rank}(x) = \operatorname{rank}(y) $$$$

Lean4

theorem rank_congr : ∀ {x y : PSet}, Equiv x y → rank x = rank y
  | ⟨_, _⟩, ⟨_, _⟩, ⟨αβ, βα⟩ => by
    apply congr_arg sSup
    ext
    constructor <;> simp only [Set.mem_range, forall_exists_index] <;> intro a h
    · obtain ⟨b, h'⟩ := αβ a
      exists b
      rw [← h, rank_congr h']
    · obtain ⟨b, h'⟩ := βα a
      exists b
      rw [← h, rank_congr h']

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