English
In a SetLike structure, CovBy K L holds if and only if K < L and for all H,g, if K ≤ H ≤ L and g ∉ K but g ∈ H, then H = L.
Русский
В структуре SetLike CovBy K L выполняется тогда, когда K < L и для всех H,g, если K ≤ H ≤ L и g ∉ K, но g ∈ H, то H = L.
LaTeX
$$$ \\mathrm{CovBy}(K,L) \\iff K < L \\land \\forall H\\, g,\\ K \\le H \\to H \\le L \\to g \\notin K \\to g \\in H \\to H = L.$$$
Lean4
theorem covBy_iff {K L : A} : K ⋖ L ↔ K < L ∧ ∀ H g, K ≤ H → H ≤ L → g ∉ K → g ∈ H → H = L :=
by
refine and_congr_right fun _ ↦ forall_congr' fun H ↦ not_iff_not.mp ?_
push_neg
rw [lt_iff_le_not_ge, lt_iff_le_and_ne, and_and_and_comm]
simp_rw [exists_and_left, and_assoc, and_congr_right_iff, ← and_assoc, and_comm, exists_and_left,
SetLike.not_le_iff_exists, and_comm, implies_true]
