isRegular_iff — Mathlib

English

An element a of the product ∀ i, R i is regular iff each coordinate a i is regular.

Русский

Элемент a из произведения ∏ i R i является регулярным тогда и только тогда, когда каждая координата a i является регулярной.

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem isRegular_iff {a : ∀ i, R i} : IsRegular a ↔ ∀ i, IsRegular (a i) := by simp [_root_.isRegular_iff, forall_and]

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