isRightRegular_iff — Mathlib

English

Let a : ∀ i, R i. Then IsRightRegular a holds iff ∀ i, IsRightRegular (a i).

Русский

Пусть a : ∀ i, R i. Тогда IsRightRegular a эквивалентно ∀ i, IsRightRegular (a i).

LaTeX

$$$IsRightRegular\,a \iff \forall i, IsRightRegular(a i)$$$

Lean4

@[to_additive (attr := simp)]
theorem isRightRegular_iff {a : ∀ i, R i} : IsRightRegular a ↔ ∀ i, IsRightRegular (a i) :=
  have (i : _) : Nonempty (R i) := ⟨a i⟩;
  .symm <| Pi.map_injective.symm

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