congr — Mathlib

English

If l.HasBasis p s, and p ≡ p' and s ≡ s' (pointwise), then l.HasBasis p' s'.

Русский

Если имеем HasBasis p s и p ≡ p' и s ≡ s' по точкам, то l.HasBasis p' s'.

LaTeX

$$$l.HasBasis p s \rightarrow (\forall i, p i \leftrightarrow p' i) \rightarrow (\forall i, p i \rightarrow s i = s' i) \rightarrow l.HasBasis p' s'$$$

Lean4

protected theorem congr (hl : l.HasBasis p s) {p' s'} (hp : ∀ i, p i ↔ p' i) (hs : ∀ i, p i → s i = s' i) :
    l.HasBasis p' s' :=
  ⟨fun t ↦ by simp only [hl.mem_iff, ← hp]; exact exists_congr fun i ↦ and_congr_right fun hi ↦ hs i hi ▸ Iff.rfl⟩

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