mono — Mathlib

English

If A ⊆ B and IsCorner A x1 y1 x2 y2 holds, then IsCorner B x1 y1 x2 y2 also holds.

Русский

Если A ⊆ B и IsCorner A x1 y1 x2 y2, тогда IsCorner B x1 y1 x2 y2 тоже выполняется.

LaTeX

$$IsCorner A x1 y1 x2 y2 ∧ A ⊆ B ⇒ IsCorner B x1 y1 x2 y2$$

Lean4

theorem mono (hAB : A ⊆ B) (hA : IsCorner A x₁ y₁ x₂ y₂) : IsCorner B x₁ y₁ x₂ y₂
    where
  fst_fst_mem := hAB hA.fst_fst_mem
  fst_snd_mem := hAB hA.fst_snd_mem
  snd_fst_mem := hAB hA.snd_fst_mem
  add_eq_add := hA.add_eq_add

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