mono — Mathlib

English

If s ⊆ t and x,y are fixed, then visibility through t implies visibility through s.

Русский

Если s ⊆ t и пары точек фиксированы, то через больший набор t видимость влечёт видимость через меньший s.

LaTeX

$$s ⊆ t → IsVisible 𝕜 t x y → IsVisible 𝕜 s x y$$

Lean4

theorem mono (hst : s ⊆ t) (ht : IsVisible 𝕜 t x y) : IsVisible 𝕜 s x y := fun _z hz ↦ ht <| hst hz

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