mono — Mathlib

English

If A is extreme in C, B ⊆ A, and C ⊆ B, then B is extreme in C.

Русский

Если A крайнее в C, а B ⊆ A и C ⊆ B, то B крайнее в C.

LaTeX

$$$B \subseteq A\quad\text{and}\quad C \subseteq B\quad\text{and}\quad IsExtreme 𝕜 A C\Rightarrow IsExtreme 𝕜 B C$$$

Lean4

protected theorem mono (hAC : IsExtreme 𝕜 A C) (hBA : B ⊆ A) (hCB : C ⊆ B) : IsExtreme 𝕜 B C :=
  ⟨hCB, fun _ hx₁B _ hx₂B _ hxC hx ↦ hAC.2 (hBA hx₁B) (hBA hx₂B) hxC hx⟩

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