mabs_by_cases

Mathlib.Algebra.Order.Group.Unbundled.Abs

URI: https://scilib.ai/kg/mathlib#mabs_by_cases

English

For any predicate P on α, if P(a) and P(a^{-1}) hold, then P(|a|_m).

Русский

Для любого предиката P на α, если P(a) и P(a^{-1}) верны, то P(|a|_m).

LaTeX

$$$(\forall a\in α)(P(a) \land P(a^{-1}) \Rightarrow P(|a|_m))$$$

Lean4

@[to_additive]
theorem mabs_by_cases (P : α → Prop) (h1 : P a) (h2 : P a⁻¹) : P |a|ₘ :=
  sup_ind _ _ h1 h2

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru