subset_congr_right

Mathlib.Data.List.Perm.Basic

URI: https://scilib.ai/kg/mathlib#List.Perm.subset_congr_right

English

If l1 ~ l2, then subsets relative to l3 satisfy l3 ⊆ l1 iff l3 ⊆ l2.

Русский

Если l1 ~ l2, тогда l3 ⊆ l1 эквивалентно l3 ⊆ l2.

LaTeX

$$$l_1 \\sim l_2 \\Rightarrow (l_3 \\subseteq l_1) \\iff (l_3 \\subseteq l_2).$$$

Lean4

theorem subset_congr_right {l₁ l₂ l₃ : List α} (h : l₁ ~ l₂) : l₃ ⊆ l₁ ↔ l₃ ⊆ l₂ :=
  ⟨fun h' => h'.trans h.subset, fun h' => h'.trans h.symm.subset⟩

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

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

Разделы

Аффилиация

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