congr — Mathlib

English

The separating-left property is equivalent under a change of coordinates by a pair of linear equivalences.

Русский

Свойство разделения слева эквивалентно после смены координат двумя линейными эквивалентностями.

LaTeX

$$((e1.arrowCongr (e2.arrowCongr (LinearEquiv.refl R M)) B).SeparatingLeft) ↔ (B.SeparatingLeft)$$

Lean4

theorem congr (h : B.SeparatingLeft) : (e₁.arrowCongr (e₂.arrowCongr (LinearEquiv.refl R M)) B).SeparatingLeft :=
  by
  intro x hx
  rw [← e₁.symm.map_eq_zero_iff]
  refine h (e₁.symm x) fun y ↦ ?_
  specialize hx (e₂ y)
  simp only [LinearEquiv.arrowCongr_apply, LinearEquiv.symm_apply_apply, LinearEquiv.map_eq_zero_iff] at hx
  exact hx

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