mono — Mathlib

English

If A is exposed to C and B ⊆ A and C ⊆ B, then B is exposed to C.

Русский

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

LaTeX

$$$\\mathrm{IsExposed}\\ 𝕜\\ A\\C \\to B\\subseteq A \\to C\\subseteq B \\to \\mathrm{IsExposed}\\ 𝕜\\ B\\ C$$$

Lean4

protected theorem mono (hC : IsExposed 𝕜 A C) (hBA : B ⊆ A) (hCB : C ⊆ B) : IsExposed 𝕜 B C :=
  by
  rintro ⟨w, hw⟩
  obtain ⟨l, rfl⟩ := hC ⟨w, hw⟩
  exact
    ⟨l,
      Subset.antisymm (fun x hx => ⟨hCB hx, fun y hy => hx.2 y (hBA hy)⟩) fun x hx =>
        ⟨hBA hx.1, fun y hy => (hw.2 y hy).trans (hx.2 w (hCB hw))⟩⟩

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