bijOn_iff — Mathlib

English

Given BijOn f s t, a universal quantification over t is equivalent to a universal quantification over s via f.

Русский

При наличии BijOn f s t эквивалентно выражение для всех b∈t свойство через все a∈s через f.

LaTeX

$$$\\text{BijOn}(f,s,t) \\Rightarrow (\\forall b\\in t\\, P(b) \\iff \\forall a\\in s\\, P(f(a)))$$$

Lean4

theorem bijOn_iff (H : EqOn f₁ f₂ s) : BijOn f₁ s t ↔ BijOn f₂ s t :=
  ⟨fun h => h.congr H, fun h => h.congr H.symm⟩

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