not_or is Demorgan's law but not_and is something unrelated?

Stream: new members

[Yagub Aliyev]

Dear friends
I am new here. I am working on completion of Natural Number Game and Set Theory Game without asking anyone. But I noticed some irregularity in naming of logic proofs and decided to ask. For example, not_or is De Morgan's law. One would expect not_and be a similar property for \and=∧ but no! It gives x ∈ A → x ∉ B when applied to ¬(x ∈ A ∧ x ∈ B)
What is the reason for this naming? And if possible how do I prove ¬(x ∈ A ∧ x ∈ B) is x ∉ A ∨ x ∉ B without not_and?

[Mario Carneiro]

it's called docs#not_and_or, or docs#Decidable.not_and in std

[Yagub Aliyev]

How to find other such names easily without asking here? Like distributivity of And over Or and vice versa?
x ∈ A ∧ (x ∈ B ∨ x ∈ C) is equivalent to
x ∈ A ∧ x ∈ B ∨ x ∈ A ∧ x ∈ C

[Ruben Van de Velde]

You can write

import Mathlib
example {α x} {A B C : Set α}: x ∈ A ∧ (x ∈ B ∨ x ∈ C) <-> x ∈ A ∧ x ∈ B ∨ x ∈ A ∧ x ∈ C := by
  exact?

[Ruben Van de Velde]

Or guess the name (#naming)

[Kevin Buzzard]

I'm not sure I want to guarantee that all names in NNG are the same as the corresponding mathlib names, although the vast majority will be.

[Kevin Buzzard]

See for example this thread.