swap_le_swap_iff — Mathlib

English

For two concepts c and d, c.swap ≤ d.swap if and only if d ≤ c. The swap operation reverses the order.

Русский

Для двух концептов c и d, c.swap ≤ d.swap если и только если d ≤ c. Операция обмена порядком разворачивает упорядочение.

LaTeX

$$$$ c.swap \le d.swap \;\iff\; d \le c. $$$$

Lean4

@[simp]
theorem swap_le_swap_iff : c.swap ≤ d.swap ↔ d ≤ c :=
  intent_subset_intent_iff

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