forall_lt_mono — Mathlib

English

If s ≤ t in Colex and every element of t is < a, then every element of s is < a.

Русский

Если s ≤ t в Colex и каждый элемент t < a, то каждый элемент s < a.

LaTeX

$$$s \le t \land \forall b \in t, b < a \Rightarrow \forall b \in s, b < a$$$

Lean4

/-- If `s ≤ t` in colex, and all elements in `t` are small, then all elements in `s` are small. -/
theorem forall_lt_mono (hst : toColex s ≤ toColex t) (ht : ∀ b ∈ t, b < a) : ∀ b ∈ s, b < a :=
  by
  rintro b hb
  by_cases b ∈ t
  · exact ht _ ‹_›
  · obtain ⟨c, hct, -, hbc⟩ := hst hb ‹_›
    exact hbc.trans_lt <| ht _ hct

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