le_mul_congr

Mathlib.Computability.Language

URI: https://scilib.ai/kg/mathlib#Language.le_mul_congr

← MathLib Explorer

English

If l1 ≤ m1 and l2 ≤ m2, then l1 * l2 ≤ m1 * m2.

Русский

Если l1 ⊆ m1 и l2 ⊆ m2, то l1 * l2 ⊆ m1 * m2.

LaTeX

$$$ l_1 \le m_1 \to l_2 \le m_2 \to l_1 * l_2 \le m_1 * m_2 $$$

Lean4

theorem le_mul_congr {l₁ l₂ m₁ m₂ : Language α} : l₁ ≤ m₁ → l₂ ≤ m₂ → l₁ * l₂ ≤ m₁ * m₂ :=
  by
  intro h₁ h₂ x hx
  simp only [mul_def, mem_image2] at hx ⊢
  tauto

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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