inseparable_pi — Mathlib

English

Let f and g be families of objects indexed by i, f,g: ∀i A_i. Then f ~ᵢ g if and only if ∀ i, f(i) ~ᵢ g(i).

Русский

Пусть f и g — семейства объектов, индексируемые по i, f,g: ∀i A_i. Тогда f ~ᵢ g тогда и только тогда, когда для каждого i выполнено f(i) ~ᵢ g(i).

LaTeX

$$$\\left( f \\sim_i g \\right) \\iff \\forall i, \\left( f(i) \\sim_i g(i) \\right).$$$

Lean4

@[simp]
theorem inseparable_pi {f g : ∀ i, A i} : (f ~ᵢ g) ↔ ∀ i, f i ~ᵢ g i := by
  simp only [Inseparable, nhds_pi, funext_iff, pi_inj]

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